no goals
α : Type u_1
β : Type ?u.190785
γ : Type ?u.190788
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o o' : Ordinal
ho : o < type r
ho' : o' < type r
⊢ ¬r (enum r o' ho') (enum r o ho) ↔ o ≤ o'
rw [← @not_lt _ _ o' o, enum_lt_enum ho']