Let a, x, y and r be given.
Assume HaS: SNo a.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume HrS: SNo r.
Assume Hrpos: 0 < r.
Assume Hamargin: a < add_SNo x (minus_SNo r).
Assume Hab: abs_SNo (add_SNo x (minus_SNo y)) < r.
We prove the intermediate claim HxmrS: SNo (add_SNo x (minus_SNo r)).
An exact proof term for the current goal is (SNo_add_SNo x (minus_SNo r) HxS (SNo_minus_SNo r HrS)).
We prove the intermediate claim HtS: SNo (add_SNo x (minus_SNo y)).
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 Hxy_lt_r: add_SNo x (minus_SNo y) < r.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt (add_SNo x (minus_SNo y)) r HtS HrS Hrpos Hab).
We prove the intermediate claim Hx_lt_ry: x < add_SNo r y.
An exact proof term for the current goal is (add_SNo_minus_Lt1 x y r HxS HyS HrS Hxy_lt_r).
We prove the intermediate claim Hx_lt_yr: x < add_SNo y r.
rewrite the current goal using (add_SNo_com r y HrS HyS) (from right to left).
An exact proof term for the current goal is Hx_lt_ry.
We prove the intermediate claim Hxmr_lt_y: add_SNo x (minus_SNo r) < y.
An exact proof term for the current goal is (add_SNo_minus_Lt1b x r y HxS HrS HyS Hx_lt_yr).
An exact proof term for the current goal is (SNoLt_tra a (add_SNo x (minus_SNo r)) y HaS HxmrS HyS Hamargin Hxmr_lt_y).
∎