∀ {α : Type u_1} (cut : α → Ordering) (x : Option α) (c : Batteries.RBColor) (a : Batteries.RBNode α) (y : α)
  (b : Batteries.RBNode α),
  Batteries.RBNode.lowerBound? cut (Batteries.RBNode.node c a y b) x =
    match cut y with
    | Ordering.lt => Batteries.RBNode.lowerBound? cut a x
    | Ordering.gt => Batteries.RBNode.lowerBound? cut b (some y)
    | Ordering.eq => some y