Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply CSNo_ReIm_split with
mul_CSNo x0 (mul_CSNo x1 x2),
mul_CSNo (mul_CSNo x0 x1) x2 leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0,
mul_CSNo x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
mul_CSNo x0 x1,
x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
set y3 to be ...
Let x4 of type ι → ο be given.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with
x1,
mul_CSNo x2 y3,
λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y5 to be ...
set y6 to be ...
Apply L12 with
λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H13: y6 y5 y5.
The subproof is completed by applying H13.
Apply add_SNo_rotate_4_0312 with
mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Re x4) (CSNo_Re y5)),
minus_SNo (mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Im x4) (CSNo_Im y5))),
minus_SNo (mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Re x4) (CSNo_Im y5))),
minus_SNo (mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Im x4) (CSNo_Re y5))),
λ x7 . y6 leaving 5 subgoals.
Apply SNo_mul_SNo_3 with
CSNo_Re y3,
CSNo_Re x4,
CSNo_Re y5 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Im x4) (CSNo_Im y5)).
Apply SNo_mul_SNo_3 with
CSNo_Re y3,
CSNo_Im x4,
CSNo_Im y5 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
The subproof is completed by applying H11.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Re x4) (CSNo_Im y5)).
Apply SNo_mul_SNo_3 with
CSNo_Im y3,
CSNo_Re x4,
CSNo_Im y5 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L7.
The subproof is completed by applying H11.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Im x4) (CSNo_Re y5)).
Apply SNo_mul_SNo_3 with
CSNo_Im y3,
CSNo_Im x4,
CSNo_Re y5 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
The subproof is completed by applying L8.
set y7 to be ...
Let x8 of type ι → ο be given.
set y9 to be ...
set y10 to be ...
Apply L14 with
λ x11 . y10 ... ... ⟶ y10 y9 x11 leaving 2 subgoals.
set y8 to be λ x8 . y7
Apply L13 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H14: y8 y7 y7.
The subproof is completed by applying H14.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with
mul_CSNo y5 y6,
y7,
λ x9 x10 . (λ x11 . y8) x10 x9 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L4.
The subproof is completed by applying L13.
Let x4 of type ι → ι → ο be given.
Apply L11 with
λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H12: x4 y3 y3.
The subproof is completed by applying H12.