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.
We prove the intermediate claim HnegS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim Hle: minus_SNo t ≤ 0.
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim HnegLe: minus_SNo t ≤ minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Le_contra 0 t SNo_0 HtS H0let).
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is HnegLe.
An exact proof term for the current goal is (SNoLeLt_tra (minus_SNo t) 0 r HnegS SNo_0 HrS Hle Hrpos).
Assume Hn0let: ¬ (0 ≤ t).
rewrite the current goal using (not_nonneg_abs_SNo t Hn0let) (from right to left) at position 1.
An exact proof term for the current goal is Hab.
∎