Let m be given.

Assume Hm: m ∈ ω.

Let p be given.

Assume Hneg H0 Hpos.

We prove the intermediate claim L1: ∀k, nat_p k → m = ordsucc k → p.

Let k be given.

Assume Hk HmSk.

An exact proof term for the current goal is Hpos k (nat_p_omega k Hk) HmSk.

An exact proof term for the current goal is nat_inv_impred (λk ⇒ m = k → p) H0 L1 m (omega_nat_p m Hm) (λq H ⇒ H).

Let m be given.

Assume Hm: m ∈ ω.

Let p be given.

Assume Hneg: ∀k ∈ ω, - m = - ordsucc k → p.

Assume H0: - m = 0 → p.

Assume Hpos: ∀k ∈ ω, - m = ordsucc k → p.

We prove the intermediate claim L2: m = 0 → p.

Assume Hm0.

Apply H0 to the current goal.

rewrite the current goal using Hm0 (from left to right).

An exact proof term for the current goal is minus_SNo_0.

We prove the intermediate claim L3: ∀k, nat_p k → m = ordsucc k → p.

Let k be given.

Assume Hk HmSk.

Apply Hneg k (nat_p_omega k Hk) to the current goal.

We will prove - m = - ordsucc k.

Use f_equal.

An exact proof term for the current goal is HmSk.

Apply nat_inv_impred (λk ⇒ m = k → p) L2 L3 m (omega_nat_p m Hm) (λq H ⇒ H) to the current goal.