no goals
α : Type ?u.106843
β : Type ?u.106846
γ : Type ?u.106849
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
h : IsLimit o
a : Ordinal
⊢ ¬a < f o ↔ ¬∃ b, b < o ∧ a < f b
simpa only [exists_prop, not_exists, not_and, not_lt] using H.2 _ h a