Let x be given.
Assume Hx.
Apply xm (0 ≤ x) to the current goal.
Assume H1.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
An exact proof term for the current goal is Hx.
Assume H1.
rewrite the current goal using not_nonneg_abs_SNo x H1 (from left to right).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
∎