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).
Use reflexivity.
Assume Hn0le: ¬ (0 ≤ x).
rewrite the current goal using (not_nonneg_abs_SNo x Hn0le) (from left to right).
rewrite the current goal using (mul_SNo_minus_minus x x HxS HxS) (from left to right).
Use reflexivity.
∎