Let n be given.
Assume Hn.
Set L to be the term {0}.
Set R to be the term {eps_ m|m ∈ n}.
We prove the intermediate claim Ln: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw.
rewrite the current goal using SingE 0 w Hw (from left to right).
An exact proof term for the current goal is SNo_0.
Let z be given.
Assume Hz.
Apply ReplE_impred n eps_ z Hz to the current goal.
Let m be given.
Assume Hm1: m ∈ n.
Assume Hm2: z = eps_ m.
rewrite the current goal using Hm2 (from left to right).
Apply SNo_eps_ to the current goal.
We will prove m ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_p_trans n Ln m Hm1.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
Apply ReplE_impred n eps_ z Hz to the current goal.
Let m be given.
Assume Hm1: m ∈ n.
Assume Hm2: z = eps_ m.
rewrite the current goal using SingE 0 w Hw (from left to right).
rewrite the current goal using Hm2 (from left to right).
We will prove 0 < eps_ m.
Apply SNo_eps_pos to the current goal.
We will prove m ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_p_trans n Ln m Hm1.
∎