Let x be given.
Assume HxS: SNo x.
Assume Habs0: abs_SNo x = 0.
Apply (xm (0 ≤ x) (x = 0)) to the current goal.
Assume H0le: 0 ≤ x.
rewrite the current goal using (nonneg_abs_SNo x H0le) (from right to left).
An exact proof term for the current goal is Habs0.
Assume Hn0le: ¬ (0 ≤ x).
We prove the intermediate claim Hm0: minus_SNo x = 0.
rewrite the current goal using (not_nonneg_abs_SNo x Hn0le) (from right to left).
An exact proof term for the current goal is Habs0.
We prove the intermediate claim Hsum: add_SNo (minus_SNo x) x = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv x HxS).
We prove the intermediate claim H0x0: add_SNo 0 x = 0.
rewrite the current goal using Hm0 (from right to left) at position 1.
An exact proof term for the current goal is Hsum.
rewrite the current goal using (add_SNo_0L x HxS) (from right to left).
An exact proof term for the current goal is H0x0.
∎