Assume Hn0le: ¬ (0 ≤ x).

rewrite the current goal using (not_nonneg_abs_SNo x Hn0le) (from left to right).

We prove the intermediate claim Hxlt0: x < 0.

Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (x < 0)) to the current goal.

Assume H: x < 0.

An exact proof term for the current goal is H.

Assume Hx0: x = 0.

We prove the intermediate claim H0le0: 0 ≤ x.

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

An exact proof term for the current goal is (SNoLe_ref 0).

An exact proof term for the current goal is (FalseE (Hn0le H0le0) (x < 0)).

Assume H0ltx: 0 < x.

We prove the intermediate claim H0lex: 0 ≤ x.

An exact proof term for the current goal is (SNoLtLe 0 x H0ltx).

An exact proof term for the current goal is (FalseE (Hn0le H0lex) (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 H0lemx: 0 ≤ minus_SNo x.

rewrite the current goal using minus_SNo_0 (from right to left) at position 1.

An exact proof term for the current goal is (minus_SNo_Le_contra x 0 HxS SNo_0 Hxle0).

An exact proof term for the current goal is (SNoLe_tra x 0 (minus_SNo x) HxS SNo_0 (SNo_minus_SNo x HxS) Hxle0 H0lemx).