Let t and u be given.
Assume HtS: SNo t.
Assume HuS: SNo u.
Assume Hlo: minus_SNo u ≤ t.
Assume Hhi: t ≤ u.
Apply (xm (0 ≤ t)) to the current goal.
Assume H0le: 0 ≤ t.
rewrite the current goal using (nonneg_abs_SNo t H0le) (from left to right).
An exact proof term for the current goal is Hhi.
Assume Hn0le: ¬ (0 ≤ t).
rewrite the current goal using (not_nonneg_abs_SNo t Hn0le) (from left to right).
We prove the intermediate claim Hmtleu: minus_SNo t ≤ u.
We prove the intermediate claim HmHlo: minus_SNo t ≤ minus_SNo (minus_SNo u).
An exact proof term for the current goal is (minus_SNo_Le_contra (minus_SNo u) t (SNo_minus_SNo u HuS) HtS Hlo).
rewrite the current goal using (minus_SNo_invol u HuS) (from right to left) at position 1.
An exact proof term for the current goal is HmHlo.
An exact proof term for the current goal is Hmtleu.
∎