no goals
α : Type u_1
β : Type ?u.188363
γ : Type ?u.188366
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x x' : α
⊢ typein r x ≤ typein r x' ↔ ¬r x' x
rw [← not_lt, typein_lt_typein]