no goals
α : Type ?u.211340
β : Type ?u.211343
γ : Type ?u.211346
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : IsLimit c
⊢ a < b * c ↔ ∃ c', c' < c ∧ a < b * c'
simpa only [not_ball, not_le, bex_def] using not_congr (@mul_le_of_limit b c a h)