Let k be given.
Assume Hk.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
We prove the intermediate
claim Lek2:
eps_ k ∈ SNoS_ ω.
An exact proof term for the current goal is SNo_eps_SNoS_omega k Hk.
Apply nat_ind to the current goal.
We will
prove eps_ k * 0 ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_zeroR (eps_ k) Lek (from left to right).
We will
prove 0 ∈ SNoS_ ω.
An exact proof term for the current goal is omega_SNoS_omega 0 (nat_p_omega 0 nat_0).
Let n be given.
Assume Hn.
We will
prove eps_ k * ordsucc n ∈ SNoS_ ω.
rewrite the current goal using add_SNo_1_ordsucc n (nat_p_omega n Hn) (from right to left).
We will
prove eps_ k * (n + 1) ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_distrL (eps_ k) n 1 Lek (omega_SNo n (nat_p_omega n Hn)) (omega_SNo 1 (nat_p_omega 1 nat_1)) (from left to right).
We will
prove eps_ k * n + eps_ k * 1 ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_oneR (eps_ k) Lek (from left to right).
We will
prove eps_ k * n + eps_ k ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is IHn.
An exact proof term for the current goal is SNo_eps_SNoS_omega k Hk.