∀ {α : Type u_1} (cmp : α → α → Ordering) (t : Batteries.RBNode α) (l r : Option α),
  Batteries.RBNode.isOrdered cmp t l r =
    match t with
    | Batteries.RBNode.nil =>
      match l, r with
      | some l, some r => decide (cmp l r = Ordering.lt)
      | x, x_1 => true
    | Batteries.RBNode.node c a v b =>
      Batteries.RBNode.isOrdered cmp a l (some v) && Batteries.RBNode.isOrdered cmp b (some v) r