a b : Ordinal
hba : b ≤ a * ω
⊢ a * ω ≤ nfp ((fun x x_1 => x + x_1) a) b

a b : Ordinal
hba : b ≤ a * ω
⊢ (fun x x_1 => x + x_1) a (a * ω) ≤ a * ω
a b : Ordinal
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) b = a * ω
apply le_antisymm (nfp_le_fp (add_isNormal a).monotone hba _)
a b : Ordinal
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) 0 ≤ nfp ((fun x x_1 => x + x_1) a) b
a b : Ordinal
hba : b ≤ a * ω
⊢ a * ω ≤ nfp ((fun x x_1 => x + x_1) a) b
rw [← nfp_add_zero]
no goals
a b : Ordinal
hba : b ≤ a * ω
⊢ nfp (fun x => a + x) 0 ≤ nfp ((fun x x_1 => x + x_1) a) b
exact nfp_monotone (add_isNormal a).monotone (Ordinal.zero_le b)
a b : Ordinal
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω
a b : Ordinal
hba : b ≤ a * ω
⊢ (fun x x_1 => x + x_1) a (a * ω) ≤ a * ω
dsimp
no goals
a b : Ordinal
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω
rw [← mul_one_add, one_add_omega]