Let x0 of type ι be given.
Let x1 of type ι be given.
Apply real_SNo with
x0.
The subproof is completed by applying H0.
Apply real_SNo with
x1.
The subproof is completed by applying H1.
Apply SNoLt_trichotomy_or_impred with
x0,
0,
mul_SNo x0 x1 ∈ real leaving 5 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Apply minus_SNo_Lt_contra2 with
x0,
0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Apply minus_SNo_0 with
λ x2 x3 . SNoLt x0 x3.
The subproof is completed by applying H4.
Apply SNoLt_trichotomy_or_impred with
x1,
0,
mul_SNo x0 x1 ∈ real leaving 5 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying SNo_0.
Apply mul_SNo_minus_minus with
x0,
x1,
λ x2 x3 . x2 ∈ real leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply real_mul_SNo_pos with
minus_SNo x0,
minus_SNo x1 leaving 4 subgoals.
Apply real_minus_SNo with
x0.
The subproof is completed by applying H0.
Apply real_minus_SNo with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying L5.
Apply minus_SNo_Lt_contra2 with
x1,
0 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying SNo_0.
Apply minus_SNo_0 with
λ x2 x3 . SNoLt x1 x3.
The subproof is completed by applying H6.
Assume H6: x1 = 0.
Apply H6 with
λ x2 x3 . mul_SNo x0 x3 ∈ real.
Apply mul_SNo_zeroR with
x0,
λ x2 x3 . x3 ∈ real leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying real_0.
Apply minus_SNo_invol with
mul_SNo x0 x1,
λ x2 x3 . x2 ∈ real leaving 2 subgoals.
Apply SNo_mul_SNo with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply mul_SNo_minus_distrL with
x0,
x1,
λ x2 x3 . minus_SNo x2 ∈ real leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply real_minus_SNo with
mul_SNo (minus_SNo x0) x1.
Apply real_mul_SNo_pos with
minus_SNo x0,
x1 leaving 4 subgoals.
Apply real_minus_SNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L5.
The subproof is completed by applying H6.
Assume H4: x0 = 0.
Apply H4 with
λ x2 x3 . mul_SNo x3 x1 ∈ real.
Apply mul_SNo_zeroL with
x1,
λ x2 x3 . x3 ∈ real leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying real_0.
Apply SNoLt_trichotomy_or_impred with
x1,
0,
mul_SNo x0 x1 ∈ real leaving 5 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying SNo_0.
Apply minus_SNo_invol with
mul_SNo x0 x1,
λ x2 x3 . x2 ∈ real leaving 2 subgoals.
Apply SNo_mul_SNo with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply mul_SNo_minus_distrR with
x0,
x1,
λ x2 x3 . minus_SNo x2 ∈ real leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply real_minus_SNo with
mul_SNo x0 (minus_SNo x1).
Apply real_mul_SNo_pos with
x0,
minus_SNo x1 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply real_minus_SNo with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply minus_SNo_Lt_contra2 with
x1,
0 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying SNo_0.
Apply minus_SNo_0 with
λ x2 x3 . SNoLt x1 x3.
The subproof is completed by applying H5.
Assume H5: x1 = 0.
Apply H5 with
λ x2 x3 . mul_SNo x0 x3 ∈ real.
Apply mul_SNo_zeroR with
x0,
λ x2 x3 . x3 ∈ real leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying real_0.
Apply real_mul_SNo_pos with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.