no goals
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
xy : cmp x y = Ordering.lt
hx : cut x = Ordering.gt
⊢ ∀ {x : α}, x ∈ none → All (fun x_1 => cmpLT cmp x x_1) t
exact fun.