Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is real_SNo x Hx.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is real_SNo y Hy.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Lx Ly.
Apply SNoLt_trichotomy_or_impred x 0 Lx SNo_0 to the current goal.
Assume H1: x < 0.
We prove the intermediate claim Lmx: 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Lx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
Apply SNoLt_trichotomy_or_impred y 0 Ly SNo_0 to the current goal.
Assume H2: y < 0.
We will prove x * y ∈ real.
rewrite the current goal using mul_SNo_minus_minus x y Lx Ly (from right to left).
We will prove (- x) * (- y) ∈ real.
Apply real_mul_SNo_pos (- x) (real_minus_SNo x Hx) (- y) (real_minus_SNo y Hy) Lmx to the current goal.
We will prove 0 < - y.
Apply minus_SNo_Lt_contra2 y 0 Ly SNo_0 to the current goal.
We will prove y < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2.
Assume H2: y = 0.
rewrite the current goal using H2 (from left to right).
rewrite the current goal using mul_SNo_zeroR x Lx (from left to right).
An exact proof term for the current goal is real_0.
Assume H2: 0 < y.
We will prove x * y ∈ real.
rewrite the current goal using minus_SNo_invol (x * y) Lxy (from right to left).
We will prove - - (x * y) ∈ real.
rewrite the current goal using mul_SNo_minus_distrL x y Lx Ly (from right to left).
We will prove - ((- x) * y) ∈ real.
Apply real_minus_SNo to the current goal.
We will prove (- x) * y ∈ real.
An exact proof term for the current goal is real_mul_SNo_pos (- x) (real_minus_SNo x Hx) y Hy Lmx H2.
Assume H1: x = 0.
We will prove x * y ∈ real.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using mul_SNo_zeroL y Ly (from left to right).
An exact proof term for the current goal is real_0.
Assume H1: 0 < x.
Apply SNoLt_trichotomy_or_impred y 0 Ly SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using minus_SNo_invol (x * y) Lxy (from right to left).
We will prove - - (x * y) ∈ real.
rewrite the current goal using mul_SNo_minus_distrR x y Lx Ly (from right to left).
We will prove - (x * (- y)) ∈ real.
Apply real_minus_SNo to the current goal.
We will prove x * (- y) ∈ real.
Apply real_mul_SNo_pos x Hx (- y) (real_minus_SNo y Hy) H1 to the current goal.
We will prove 0 < - y.
Apply minus_SNo_Lt_contra2 y 0 Ly SNo_0 to the current goal.
We will prove y < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2.
Assume H2: y = 0.
rewrite the current goal using H2 (from left to right).
rewrite the current goal using mul_SNo_zeroR x Lx (from left to right).
An exact proof term for the current goal is real_0.
Assume H2: 0 < y.
An exact proof term for the current goal is real_mul_SNo_pos x Hx y Hy H1 H2.
∎