no goals
α : Type ?u.91204
β : Type ?u.91207
γ : Type ?u.91210
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : IsLimit o
a : Ordinal
⊢ a < o ↔ ∃ x, x < o ∧ a < x
simpa only [not_ball, not_le, bex_def] using not_congr (@limit_le _ h a)