Assume Hm1: minus_SNo 1 ∈ ω.
We will prove False.
We prove the intermediate claim Hle0: 0 ≤ minus_SNo 1.
An exact proof term for the current goal is (omega_nonneg (minus_SNo 1) Hm1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
Apply (SNoLeE 0 (minus_SNo 1) SNo_0 Hm1S Hle0 False) to the current goal.
Assume H0ltm1: 0 < minus_SNo 1.
We prove the intermediate claim Hm1lt0: minus_SNo 1 < 0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 (minus_SNo 1) 0 SNo_0 Hm1S SNo_0 H0ltm1 Hm1lt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H0eqm1: 0 = minus_SNo 1.
We prove the intermediate claim Hm1lt0: minus_SNo 1 < 0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using H0eqm1 (from left to right) at position 1.
An exact proof term for the current goal is Hm1lt0.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
∎