Let x be given.
Assume HxS: SNo x.
Assume H0lex: 0 ≤ x.
Assume Hxne0: x ≠ 0.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (0 < x)) to the current goal.
Assume Hxlt0: x < 0.
We prove the intermediate claim Hxle0: x ≤ 0.
An exact proof term for the current goal is (SNoLtLe x 0 Hxlt0).
We prove the intermediate claim H0lex': 0 ≤ x.
An exact proof term for the current goal is H0lex.
We prove the intermediate claim Heq0: x = 0.
An exact proof term for the current goal is (SNoLe_antisym x 0 HxS SNo_0 Hxle0 H0lex').
An exact proof term for the current goal is (FalseE (Hxne0 Heq0) (0 < x)).
Assume Hx0: x = 0.
An exact proof term for the current goal is (FalseE (Hxne0 Hx0) (0 < x)).
Assume H0ltx: 0 < x.
An exact proof term for the current goal is H0ltx.
∎