Let x, y and r be given.
Assume HxR: x ∈ R.
Assume HyR: y ∈ R.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hlo: Rlt (add_SNo y (minus_SNo r)) x.
Assume Hhi: Rlt x (add_SNo y r).
Set t to be the term add_SNo x (minus_SNo y).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (SNo_add_SNo x (minus_SNo y) HxS (SNo_minus_SNo y HyS)).
We prove the intermediate claim HrposS: 0 < r.
An exact proof term for the current goal is (RltE_lt 0 r Hrpos).
We prove the intermediate claim HhiLt: x < add_SNo y r.
An exact proof term for the current goal is (RltE_lt x (add_SNo y r) Hhi).
We prove the intermediate claim Hx_lt_ry: x < add_SNo r y.
rewrite the current goal using (add_SNo_com y r HyS HrS) (from right to left).
An exact proof term for the current goal is HhiLt.
We prove the intermediate claim Ht_lt_r: t < r.
An exact proof term for the current goal is (add_SNo_minus_Lt1b x y r HxS HyS HrS Hx_lt_ry).
We prove the intermediate claim HloLt: add_SNo y (minus_SNo r) < x.
An exact proof term for the current goal is (RltE_lt (add_SNo y (minus_SNo r)) x Hlo).
We prove the intermediate claim Hyr_lt_x: y < add_SNo x r.
An exact proof term for the current goal is (add_SNo_minus_Lt1 y r x HyS HrS HxS HloLt).
We prove the intermediate claim Hy_lt_rx: y < add_SNo r x.
rewrite the current goal using (add_SNo_com x r HxS HrS) (from right to left).
An exact proof term for the current goal is Hyr_lt_x.
We prove the intermediate claim Hy_minus_x_lt_r: add_SNo y (minus_SNo x) < r.
An exact proof term for the current goal is (add_SNo_minus_Lt1b y x r HyS HxS HrS Hy_lt_rx).
We prove the intermediate claim HmtEq: minus_SNo t = add_SNo y (minus_SNo x).
We will prove minus_SNo t = add_SNo y (minus_SNo x).
We prove the intermediate claim HtDef: t = add_SNo x (minus_SNo y).
Use reflexivity.
rewrite the current goal using HtDef (from left to right) at position 1.
We prove the intermediate claim HmyS: SNo (minus_SNo y).
An exact proof term for the current goal is (SNo_minus_SNo y HyS).
We prove the intermediate claim Hneg0: minus_SNo (add_SNo x (minus_SNo y)) = add_SNo (minus_SNo x) (minus_SNo (minus_SNo y)).
An exact proof term for the current goal is (minus_add_SNo_distr x (minus_SNo y) HxS HmyS).
rewrite the current goal using Hneg0 (from left to right) at position 1.
rewrite the current goal using (minus_SNo_invol y HyS) (from left to right).
We prove the intermediate claim Hcom: add_SNo (minus_SNo x) y = add_SNo y (minus_SNo x).
An exact proof term for the current goal is (add_SNo_com (minus_SNo x) y (SNo_minus_SNo x HxS) HyS).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
Apply (xm (0 ≤ t)) to the current goal.
Assume H0let: 0 ≤ t.
rewrite the current goal using (nonneg_abs_SNo t H0let) (from left to right) at position 1.
An exact proof term for the current goal is Ht_lt_r.
Assume Hn0let: ¬ (0 ≤ t).
rewrite the current goal using (not_nonneg_abs_SNo t Hn0let) (from left to right) at position 1.
rewrite the current goal using HmtEq (from left to right) at position 1.
An exact proof term for the current goal is Hy_minus_x_lt_r.
∎