Let x be given.
Assume HxS: SNo x.
Apply (xm (0 ≤ x)) to the current goal.
Assume H0le: 0 ≤ x.
rewrite the current goal using (nonneg_abs_SNo x H0le) (from left to right).
We prove the intermediate claim Hmxle0: minus_SNo x ≤ 0.
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 0 x SNo_0 HxS H0le).
An exact proof term for the current goal is (SNoLe_tra (minus_SNo x) 0 x (SNo_minus_SNo x HxS) SNo_0 HxS Hmxle0 H0le).
Assume Hn0le: ¬ (0 ≤ x).
rewrite the current goal using (not_nonneg_abs_SNo x Hn0le) (from left to right).
rewrite the current goal using (minus_SNo_invol x HxS) (from left to right).
An exact proof term for the current goal is (SNoLe_ref x).
∎