Let x be given.
Assume Hx.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
Apply orIR to the current goal.
Apply mul_SNo_neg_neg to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H1.
Assume H1: x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: 0 < x.
Apply orIR to the current goal.
Apply mul_SNo_pos_pos to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H1.
∎