α : Type ?u.259815
β : Type ?u.259818
γ : Type ?u.259821
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ a < b * (a / b) + b
α : Type ?u.259815
β : Type ?u.259818
γ : Type ?u.259821
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ b * (a / b) + a % b < b * (a / b) + b
rw [div_add_mod]
no goals
α : Type ?u.259815
β : Type ?u.259818
γ : Type ?u.259821
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ a < b * (a / b) + b
exact lt_mul_div_add a h