Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume H0lex: 0 ≤ x.
Assume H0ley: 0 ≤ y.
Assume Hsqle: mul_SNo x x ≤ mul_SNo y y.
Apply (SNoLt_trichotomy_or_impred y x HyS HxS (x ≤ y)) to the current goal.
Assume Hyltx: y < x.
We prove the intermediate claim HysqLt: mul_SNo y y < mul_SNo x x.
An exact proof term for the current goal is (SNoLt_sqr_nonneg y x HyS HxS H0ley H0lex Hyltx).
We prove the intermediate claim Hbad: mul_SNo y y < mul_SNo y y.
An exact proof term for the current goal is (SNoLtLe_tra (mul_SNo y y) (mul_SNo x x) (mul_SNo y y) (SNo_mul_SNo y y HyS HyS) (SNo_mul_SNo x x HxS HxS) (SNo_mul_SNo y y HyS HyS) HysqLt Hsqle).
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo y y)) Hbad) (x ≤ y)).
Assume Hyx: y = x.
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is (SNoLe_ref x).
Assume Hxley: x < y.
An exact proof term for the current goal is (SNoLtLe x y Hxley).
∎