Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Set u to be the term add_SNo (abs_SNo x) (abs_SNo y).
We prove the intermediate claim HabsxS: SNo (abs_SNo x).
An exact proof term for the current goal is (SNo_abs_SNo x HxS).
We prove the intermediate claim HabsyS: SNo (abs_SNo y).
An exact proof term for the current goal is (SNo_abs_SNo y HyS).
We prove the intermediate claim HuS: SNo u.
An exact proof term for the current goal is (SNo_add_SNo (abs_SNo x) (abs_SNo y) HabsxS HabsyS).
We prove the intermediate claim Hxub: x ≤ abs_SNo x.
An exact proof term for the current goal is (abs_SNo_upper_bound x HxS).
We prove the intermediate claim Hyub: y ≤ abs_SNo y.
An exact proof term for the current goal is (abs_SNo_upper_bound y HyS).
We prove the intermediate claim Hhi: add_SNo x y ≤ u.
An exact proof term for the current goal is (add_SNo_Le3 x y (abs_SNo x) (abs_SNo y) HxS HyS HabsxS HabsyS Hxub Hyub).
We prove the intermediate claim Hxlo: minus_SNo (abs_SNo x) ≤ x.
An exact proof term for the current goal is (abs_SNo_lower_bound x HxS).
We prove the intermediate claim Hylo: minus_SNo (abs_SNo y) ≤ y.
An exact proof term for the current goal is (abs_SNo_lower_bound y HyS).
We prove the intermediate claim Hlo': add_SNo (minus_SNo (abs_SNo x)) (minus_SNo (abs_SNo y)) ≤ add_SNo x y.
An exact proof term for the current goal is (add_SNo_Le3 (minus_SNo (abs_SNo x)) (minus_SNo (abs_SNo y)) x y (SNo_minus_SNo (abs_SNo x) HabsxS) (SNo_minus_SNo (abs_SNo y) HabsyS) HxS HyS Hxlo Hylo).
We prove the intermediate claim Hlo: minus_SNo u ≤ add_SNo x y.
rewrite the current goal using (minus_add_SNo_distr (abs_SNo x) (abs_SNo y) HabsxS HabsyS) (from left to right).
An exact proof term for the current goal is Hlo'.
An exact proof term for the current goal is (abs_SNo_Le_of_bounds (add_SNo x y) u (SNo_add_SNo x y HxS HyS) HuS Hlo Hhi).
∎