Let x be given.

Assume HxS: SNo x.

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

An exact proof term for the current goal is (SNo_zero_or_sqr_pos x HxS).

Apply Hcases 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 0 SNo_0) (from left to right).

An exact proof term for the current goal is (SNoLe_ref 0).

Assume Hpos: 0 < mul_SNo x x.

An exact proof term for the current goal is (SNoLtLe 0 (mul_SNo x x) Hpos).

∎