∀ {α : Type u_1} (cmp : α → α → Ordering) (x : Batteries.RBNode.Path α) (x_1 : α),
  Batteries.RBNode.Path.RootOrdered cmp x x_1 =
    match x, x_1 with
    | Batteries.RBNode.Path.root, x => True
    | Batteries.RBNode.Path.left c parent x r, v =>
      Batteries.RBNode.cmpLT cmp v x ∧ Batteries.RBNode.Path.RootOrdered cmp parent v
    | Batteries.RBNode.Path.right c l x parent, v =>
      Batteries.RBNode.cmpLT cmp x v ∧ Batteries.RBNode.Path.RootOrdered cmp parent v