Let x and y be given.
Assume Hx Hy Hxnn Hynn.
Apply SNoLeE 0 x SNo_0 Hx Hxnn to the current goal.
Assume H1: 0 < x.
Apply SNoLeE 0 y SNo_0 Hy Hynn to the current goal.
Assume H2: 0 < y.
An exact proof term for the current goal is SNo_pos_sqr_uniq x y Hx Hy H1 H2.
Assume H2: 0 = y.
rewrite the current goal using H2 (from right to left).
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from left to right).
Assume H3: x * x = 0.
We will prove x = 0.
Apply SNo_zero_or_sqr_pos x Hx to the current goal.
Assume H4: x = 0.
An exact proof term for the current goal is H4.
Assume H4: 0 < x * x.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H3 (from right to left) at position 2.
An exact proof term for the current goal is H4.
Assume H1: 0 = x.
rewrite the current goal using H1 (from right to left).
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from left to right).
Assume H2: 0 = y * y.
We will prove 0 = y.
Apply SNo_zero_or_sqr_pos y Hy to the current goal.
Assume H3: y = 0.
Use symmetry.
An exact proof term for the current goal is H3.
Assume H3: 0 < y * y.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is H3.
∎