∀ {α : Type u_1} (cut : α → Ordering) (x : Batteries.RBNode.Path α) (c : Batteries.RBColor) (a : Batteries.RBNode α)
  (y : α) (b : Batteries.RBNode α),
  Batteries.RBNode.zoom cut (Batteries.RBNode.node c a y b) x =
    match cut y with
    | Ordering.lt => Batteries.RBNode.zoom cut a (Batteries.RBNode.Path.left c x y b)
    | Ordering.gt => Batteries.RBNode.zoom cut b (Batteries.RBNode.Path.right c a y x)
    | Ordering.eq => (Batteries.RBNode.node c a y b, x)