Let x be given.

Assume Hx.

Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.

Assume H1: x < 0.

Apply SNoLtLe to the current goal.

We will prove 0 < x * x.

rewrite the current goal using mul_SNo_zeroR x Hx (from right to left).

We will prove x * 0 < x * x.

Apply neg_mul_SNo_Lt x 0 x Hx H1 SNo_0 Hx H1 to the current goal.

Assume H1: 0 ≤ x.

We will prove 0 ≤ x * x.

rewrite the current goal using mul_SNo_zeroR x Hx (from right to left).

We will prove x * 0 ≤ x * x.

An exact proof term for the current goal is nonneg_mul_SNo_Le x 0 x Hx H1 SNo_0 Hx H1.

∎