no goals
α : Type ?u.232451
β : Type ?u.232454
γ : Type ?u.232457
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b
rw [← not_le, div_le h, not_lt]