a : Ordinal
⊢ ∀ (n : ℕ), ((fun x => a * x)^[n]) 0 ≤ 0
a : Ordinal
⊢ nfp (fun x => a * x) 0 = 0
rw [← Ordinal.le_zero, nfp_le_iff]
a : Ordinal
n : ℕ
⊢ ((fun x => a * x)^[n]) 0 ≤ 0
a : Ordinal
⊢ ∀ (n : ℕ), ((fun x => a * x)^[n]) 0 ≤ 0
intro n
case zero
a : Ordinal
⊢ ((fun x => a * x)^[Nat.zero]) 0 ≤ 0

case succ
a : Ordinal
n : ℕ
hn : ((fun x => a * x)^[n]) 0 ≤ 0
⊢ ((fun x => a * x)^[Nat.succ n]) 0 ≤ 0
a : Ordinal
n : ℕ
⊢ ((fun x => a * x)^[n]) 0 ≤ 0
induction' n with n hn
case succ
a : Ordinal
n : ℕ
hn : ((fun x => a * x)^[n]) 0 ≤ 0
⊢ ((fun x => a * x)^[Nat.succ n]) 0 ≤ 0
case succ
a : Ordinal
n : ℕ
hn : ((fun x => a * x)^[n]) 0 ≤ 0
⊢ ((fun x => a * x)^[Nat.succ n]) 0 ≤ 0
dsimp only
no goals
case succ
a : Ordinal
n : ℕ
hn : ((fun x => a * x)^[n]) 0 ≤ 0
⊢ ((fun x => a * x)^[Nat.succ n]) 0 ≤ 0
rwa [iterate_succ_apply, mul_zero]
no goals
case zero
a : Ordinal
⊢ ((fun x => a * x)^[Nat.zero]) 0 ≤ 0
rfl