Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume H0lex: 0 ≤ x.
Apply (xm (0 ≤ y)) to the current goal.
Assume H0ley: 0 ≤ y.
rewrite the current goal using (nonneg_abs_SNo y H0ley) (from left to right).
We prove the intermediate claim H0lexy: 0 ≤ mul_SNo x y.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg x y HxS HyS H0lex H0ley).
rewrite the current goal using (nonneg_abs_SNo (mul_SNo x y) H0lexy) (from left to right).
Use reflexivity.
Assume Hn0ley: ¬ (0 ≤ y).
rewrite the current goal using (not_nonneg_abs_SNo y Hn0ley) (from left to right).
Apply (xm (x = 0)) to the current goal.
Assume Hx0: x = 0.
rewrite the current goal using Hx0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL y HyS) (from left to right).
rewrite the current goal using (mul_SNo_zeroL (minus_SNo y) (SNo_minus_SNo y HyS)) (from left to right).
rewrite the current goal using (nonneg_abs_SNo 0 (SNoLe_ref 0)) (from left to right).
Use reflexivity.
Assume Hxne0: x ≠ 0.
We prove the intermediate claim H0ltx: 0 < x.
We prove the intermediate claim H0or: 0 < x ∨ 0 = x.
An exact proof term for the current goal is (SNoLeE 0 x SNo_0 HxS H0lex).
Apply H0or to the current goal.
Assume H: 0 < x.
An exact proof term for the current goal is H.
Assume H0x: 0 = x.
We prove the intermediate claim Hx0: x = 0.
rewrite the current goal using H0x (from right to left).
Use reflexivity.
An exact proof term for the current goal is (FalseE (Hxne0 Hx0) (0 < x)).
We prove the intermediate claim Hylt0: y < 0.
Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (y < 0)) to the current goal.
Assume H: y < 0.
An exact proof term for the current goal is H.
Assume Hy0: y = 0.
We prove the intermediate claim H0ley: 0 ≤ y.
rewrite the current goal using Hy0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
An exact proof term for the current goal is (FalseE (Hn0ley H0ley) (y < 0)).
Assume H0lty: 0 < y.
We prove the intermediate claim H0ley: 0 ≤ y.
An exact proof term for the current goal is (SNoLtLe 0 y H0lty).
An exact proof term for the current goal is (FalseE (Hn0ley H0ley) (y < 0)).
We prove the intermediate claim Hxylt0: mul_SNo x y < 0.
rewrite the current goal using (mul_SNo_zeroR x HxS) (from right to left).
An exact proof term for the current goal is (pos_mul_SNo_Lt x y 0 HxS H0ltx HyS SNo_0 Hylt0).
We prove the intermediate claim Hn0lexy: ¬ (0 ≤ mul_SNo x y).
Assume H0le: 0 ≤ mul_SNo x y.
We prove the intermediate claim HxyS: SNo (mul_SNo x y).
An exact proof term for the current goal is (SNo_mul_SNo x y HxS HyS).
We prove the intermediate claim Hbad: mul_SNo x y < mul_SNo x y.
An exact proof term for the current goal is (SNoLtLe_tra (mul_SNo x y) 0 (mul_SNo x y) HxyS SNo_0 HxyS Hxylt0 H0le).
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo x y)) Hbad) False).
rewrite the current goal using (not_nonneg_abs_SNo (mul_SNo x y) Hn0lexy) (from left to right).
rewrite the current goal using (mul_SNo_minus_distrR x y HxS HyS) (from left to right).
Use reflexivity.
∎