Let x and y be given.
Assume Hx Hy.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using neg_abs_SNo x Hx H1 (from left to right).
Apply SNoLtLe_or y 0 Hy SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using neg_abs_SNo y Hy H2 (from left to right).
We will prove abs_SNo (x + y) ≤ - x + - y.
We prove the intermediate claim L1: x + y < 0.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove x + y < 0 + 0.
An exact proof term for the current goal is add_SNo_Lt3 x y 0 0 Hx Hy SNo_0 SNo_0 H1 H2.
rewrite the current goal using neg_abs_SNo (x + y) Lxy L1 (from left to right).
We will prove - (x + y) ≤ - x + - y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
Apply SNoLe_ref to the current goal.
Assume H2: 0 ≤ y.
rewrite the current goal using nonneg_abs_SNo y H2 (from left to right).
We will prove abs_SNo (x + y) ≤ - x + y.
Apply xm (0 ≤ x + y) to the current goal.
Assume H3.
rewrite the current goal using nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove x + y ≤ - x + y.
Apply add_SNo_Le1 x y (- x) Hx Hy Lmx to the current goal.
We will prove x ≤ - x.
Apply SNoLtLe to the current goal.
We will prove x < - x.
Apply SNoLt_tra x 0 (- x) Hx SNo_0 Lmx H1 to the current goal.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
Assume H3.
rewrite the current goal using not_nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove - (x + y) ≤ - x + y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
We will prove - x + - y ≤ - x + y.
Apply add_SNo_Le2 (- x) (- y) y Lmx Lmy Hy to the current goal.
We will prove - y ≤ y.
We prove the intermediate claim L2: - y ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is minus_SNo_Le_contra 0 y SNo_0 Hy H2.
An exact proof term for the current goal is SNoLe_tra (- y) 0 y Lmy SNo_0 Hy L2 H2.
Assume H1: 0 ≤ x.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
Apply SNoLtLe_or y 0 Hy SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using neg_abs_SNo y Hy H2 (from left to right).
We will prove abs_SNo (x + y) ≤ x + - y.
Apply xm (0 ≤ x + y) to the current goal.
Assume H3.
rewrite the current goal using nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove x + y ≤ x + - y.
Apply add_SNo_Le2 x y (- y) Hx Hy Lmy to the current goal.
We will prove y ≤ - y.
Apply SNoLtLe to the current goal.
We will prove y < - y.
Apply SNoLt_tra y 0 (- y) Hy SNo_0 Lmy H2 to the current goal.
We will prove 0 < - y.
Apply minus_SNo_Lt_contra2 y 0 Hy SNo_0 to the current goal.
We will prove y < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2.
Assume H3.
rewrite the current goal using not_nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove - (x + y) ≤ x + - y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
We will prove - x + - y ≤ x + - y.
Apply add_SNo_Le1 (- x) (- y) x Lmx Lmy Hx to the current goal.
We will prove - x ≤ x.
We prove the intermediate claim L3: - x ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is minus_SNo_Le_contra 0 x SNo_0 Hx H1.
An exact proof term for the current goal is SNoLe_tra (- x) 0 x Lmx SNo_0 Hx L3 H1.
Assume H2: 0 ≤ y.
rewrite the current goal using nonneg_abs_SNo y H2 (from left to right).
We will prove abs_SNo (x + y) ≤ x + y.
We prove the intermediate claim L1: 0 ≤ x + y.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove 0 + 0 ≤ x + y.
An exact proof term for the current goal is add_SNo_Le3 0 0 x y SNo_0 SNo_0 Hx Hy H1 H2.
rewrite the current goal using nonneg_abs_SNo (x + y) L1 (from left to right).
Apply SNoLe_ref to the current goal.
∎