Let m be given.
Assume Hm.
Let n be given.
Assume Hn Hmn.
Apply nat_inv n (omega_nat_p n Hn) to the current goal.
Assume H1: n = 0.
Apply andI to the current goal.
rewrite the current goal using Hmn (from left to right).
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is minus_SNo_0.
An exact proof term for the current goal is H1.
Assume H1.
We will prove False.
Apply H1 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: nat_p k.
Assume H1: n = ordsucc k.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLeLt_tra 0 m 0 SNo_0 (omega_SNo m Hm) SNo_0 to the current goal.
We will prove 0 ≤ m.
Apply ordinal_Subq_SNoLe 0 m ordinal_Empty (nat_p_ordinal m (omega_nat_p m Hm)) to the current goal.
We will prove 0 ⊆ m.
Apply Subq_Empty to the current goal.
We will prove m < 0.
rewrite the current goal using Hmn (from left to right).
We will prove - n < 0.
Apply minus_SNo_Lt_contra1 0 n SNo_0 (omega_SNo n Hn) to the current goal.
We will prove - 0 < n.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove 0 < n.
Apply ordinal_In_SNoLt n (nat_p_ordinal n (omega_nat_p n Hn)) to the current goal.
We will prove 0 ∈ n.
rewrite the current goal using H1 (from left to right).
We will prove 0 ∈ ordsucc k.
Apply nat_0_in_ordsucc to the current goal.
An exact proof term for the current goal is Hk.
∎