∀ {α : Type u_1} {cmp : α → α → Ordering} {c : Batteries.RBColor} {n : ℕ} {v v' : α} [Std.TransCmp cmp]
  {t : Batteries.RBNode α},
  t.Balanced c n →
    Batteries.RBNode.Ordered cmp t →
      (v' ∈ Batteries.RBNode.insert cmp t v ↔ v' ∈ t ∧ Batteries.RBNode.find? (cmp v) t ≠ some v' ∨ v' = v)