Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume H0lex: 0 ≤ x.
Assume H0ley: 0 ≤ y.
Assume Hxlt: x < y.
Apply (xm (x = 0)) to the current goal.
Assume Hx0: x = 0.
We prove the intermediate claim H0lty: 0 < y.
rewrite the current goal using Hx0 (from right to left) at position 1.
An exact proof term for the current goal is Hxlt.
We prove the intermediate claim Hy2pos: 0 < mul_SNo y y.
An exact proof term for the current goal is (mul_SNo_pos_pos y y HyS HyS H0lty H0lty).
rewrite the current goal using Hx0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).
An exact proof term for the current goal is Hy2pos.
Assume Hxne0: x ≠ 0.
We prove the intermediate claim H0ltx: 0 < x.
An exact proof term for the current goal is (SNo_nonneg_ne0_pos x HxS H0lex Hxne0).
We prove the intermediate claim H0lty: 0 < y.
An exact proof term for the current goal is (SNoLt_tra 0 x y SNo_0 HxS HyS H0ltx Hxlt).
An exact proof term for the current goal is (pos_mul_SNo_Lt2 x x y y HxS HxS HyS HyS H0ltx H0ltx Hxlt Hxlt).
∎