Let x and xi be given.
Assume Hx Hxi Hxpos Hxxi.
Apply SNoLt_trichotomy_or_impred 0 xi SNo_0 Hxi to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: 0 = xi.
We will prove False.
Apply neq_0_1 to the current goal.
We will prove 0 = 1.
rewrite the current goal using Hxxi (from right to left).
We will prove 0 = x * xi.
rewrite the current goal using H1 (from right to left).
We will prove 0 = x * 0.
Use symmetry.
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
Assume H1: xi < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLt_tra 0 1 0 SNo_0 SNo_1 SNo_0 SNoLt_0_1 to the current goal.
We will prove 1 < 0.
rewrite the current goal using Hxxi (from right to left).
We will prove x * xi < 0.
An exact proof term for the current goal is mul_SNo_pos_neg x xi Hx Hxi Hxpos H1.
∎