∀ {α : Type u_1} {cmp : α → α → Ordering} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α}
  {c : Batteries.RBColor},
  Batteries.RBNode.Ordered cmp t →
    Batteries.RBNode.Path.Ordered cmp path →
      Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t → Batteries.RBNode.Ordered cmp (path.del t c)