case a
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b

case a
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * succ b
apply le_antisymm
case a.ab
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b

case a.h
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ (fun x x_1 => x * x_1) a (a ^ ω * succ b) ≤ a ^ ω * succ b
case a
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
apply nfp_le_fp (mul_isNormal ha).monotone
case a.ab
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
case a.ab
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b
rw [mul_succ]
no goals
case a.ab
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
apply add_le_add_left hca
case a.h
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b
case a.h
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ (fun x x_1 => x * x_1) a (a ^ ω * succ b) ≤ a ^ ω * succ b
dsimp only
no goals
case a.h
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b
rw [← mul_assoc, ← opow_one_add, one_add_omega]
case a.intro
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
case a
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
cases' mul_eq_right_iff_opow_omega_dvd.1 ((mul_isNormal ha).nfp_fp ((a^omega) * b + c)) with
  d hd
case a.intro
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d
case a.intro
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
rw [hd]
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d
case a.intro
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d
apply mul_le_mul_left'
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (Mul.mul a) (a ^ ω * b + c)
⊢ succ b ≤ d
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d
have := le_nfp (Mul.mul a) ((a^omega) * b + c)
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (Mul.mul a) (a ^ ω * b + c)
⊢ succ b ≤ d
erw [hd] at this
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d
have := (add_lt_add_left hc ((a^omega) * b)).trans_le this
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d
rw [add_zero, mul_lt_mul_iff_left (opow_pos omega ha)] at this
no goals
case a.intro.bc
a c b : Ordinal
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal
hd : nfp ((fun x x_1 => x * x_1) a) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d
rwa [succ_le_iff]