case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ (b * a + c) / b ≤ a + c / b

case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ a + c / b ≤ (b * a + c) / b
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ (b * a + c) / b = a + c / b
apply le_antisymm
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ b * a + c < b * succ (a + c / b)
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ (b * a + c) / b ≤ a + c / b
apply (div_le b0).2
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ c < b * (c / b) + b
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ b * a + c < b * succ (a + c / b)
rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]
no goals
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ c < b * (c / b) + b
apply lt_mul_div_add _ b0
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ b * (c / b) ≤ c
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ a + c / b ≤ (b * a + c) / b
rw [le_div b0, mul_add, add_le_add_iff_left]
no goals
case a
α : Type ?u.240963
β : Type ?u.240966
γ : Type ?u.240969
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
c : Ordinal
⊢ b * (c / b) ≤ c
apply mul_div_le