Let t and r be given.
Assume HtS: SNo t.
Assume HrS: SNo r.
Assume Hrpos: 0 < r.
Assume Hab: abs_SNo t < r.
Apply (xm (0 ≤ t)) to the current goal.
Assume H0let: 0 ≤ t.
rewrite the current goal using (nonneg_abs_SNo t H0let) (from right to left) at position 1.
An exact proof term for the current goal is Hab.
Assume Hn0let: ¬ (0 ≤ t).
We prove the intermediate claim Htlt0: t < 0.
Apply (SNoLt_trichotomy_or_impred t 0 HtS SNo_0 (t < 0)) to the current goal.
Assume H: t < 0.
An exact proof term for the current goal is H.
Assume Ht0: t = 0.
We prove the intermediate claim H0let: 0 ≤ t.
rewrite the current goal using Ht0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
We will prove t < 0.
An exact proof term for the current goal is (FalseE (Hn0let H0let) (t < 0)).
Assume H0ltt: 0 < t.
We prove the intermediate claim H0let: 0 ≤ t.
An exact proof term for the current goal is (SNoLtLe 0 t H0ltt).
We will prove t < 0.
An exact proof term for the current goal is (FalseE (Hn0let H0let) (t < 0)).
An exact proof term for the current goal is (SNoLt_tra t 0 r HtS SNo_0 HrS Htlt0 Hrpos).
∎