Let x and y be given.
Assume Hx Hy Hxpos Hypos.
Assume H1: x * x = y * y.
Apply SNoLt_trichotomy_or_impred x y Hx Hy to the current goal.
Assume H2: x < y.
We will prove False.
Apply SNoLt_irref (x * x) to the current goal.
We will prove x * x < x * x.
rewrite the current goal using H1 (from left to right) at position 2.
We will prove x * x < y * y.
An exact proof term for the current goal is pos_mul_SNo_Lt2 x x y y Hx Hx Hy Hy Hxpos Hxpos H2 H2.
Assume H2: x = y.
An exact proof term for the current goal is H2.
Assume H2: y < x.
We will prove False.
Apply SNoLt_irref (x * x) to the current goal.
We will prove x * x < x * x.
rewrite the current goal using H1 (from left to right) at position 1.
We will prove y * y < x * x.
An exact proof term for the current goal is pos_mul_SNo_Lt2 y y x x Hy Hy Hx Hx Hypos Hypos H2 H2.
∎