Let x be given.
Assume HxR: x ∈ R.
Apply (xm (0 ≤ x)) to the current goal.
Assume H0le: 0 ≤ x.
We prove the intermediate claim Habseq: abs_SNo x = x.
An exact proof term for the current goal is (nonneg_abs_SNo x H0le).
rewrite the current goal using Habseq (from left to right).
An exact proof term for the current goal is HxR.
Assume Hn0le: ¬ (0 ≤ x).
We prove the intermediate claim HmxR: minus_SNo x ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim Habseq: abs_SNo x = minus_SNo x.
An exact proof term for the current goal is (not_nonneg_abs_SNo x Hn0le).
rewrite the current goal using Habseq (from left to right).
An exact proof term for the current goal is HmxR.
∎