Let x and y be given.

Assume HxS: SNo x.

Assume HyS: SNo y.

Assume H0lex: 0 ≤ x.

Assume Hxlt: x < y.

We prove the intermediate claim H0lt_or_eq: 0 < x ∨ 0 = x.

We prove the intermediate claim H0x: 0 < x ∨ 0 = x.

An exact proof term for the current goal is (SNoLeE 0 x SNo_0 HxS H0lex).

An exact proof term for the current goal is H0x.

Apply H0lt_or_eq to the current goal.

Assume H0ltx: 0 < x.

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).

Assume H0eqx: 0 = x.

We prove the intermediate claim H0lt_y: 0 < y.

rewrite the current goal using H0eqx (from left to right) at position 1.

An exact proof term for the current goal is Hxlt.

rewrite the current goal using H0eqx (from right to left).

rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).

An exact proof term for the current goal is (mul_SNo_pos_pos y y HyS HyS H0lt_y H0lt_y).

∎