a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ (a + b) * succ c' ≤ a * c
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ (a + b) * c' ≤ a * c
apply (mul_le_mul_left' (le_succ c') _).trans
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ a * succ c' + b ≤ a * c
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ (a + b) * succ c' ≤ a * c
rw [IH _ h]
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ a * succ c' + ?m.427842 ≤ a * c

a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ Ordinal

a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ b ≤ ?m.427842
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ a * succ c' + b ≤ a * c
apply (add_le_add_left _ _).trans
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ a * succ (succ c') ≤ a * c
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ a * succ c' + ?m.427842 ≤ a * c
rw [← mul_succ]
no goals
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ a * succ (succ c') ≤ a * c
exact mul_le_mul_left' (succ_le_of_lt <| l.2 _ h) _
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ b ≤ b + a
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ b ≤ a
rw [← ba]
no goals
a b c : Ordinal
ba : b + a = a
l : IsLimit c
IH : ∀ (c' : Ordinal), c' < c → (a + b) * succ c' = a * succ c' + b
c' : Ordinal
h : c' < c
⊢ b ≤ b + a
exact le_add_right _ _