no goals
α : Type ?u.230000
β : Type ?u.230003
γ : Type ?u.230006
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ a < b * (a / b) + b
simpa only [mul_succ] using lt_mul_succ_div a h