Let x0 of type ι be given.
Let x1 of type ι be given.
Apply CSNo_Im2 with
add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1))),
add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)) leaving 2 subgoals.
Apply unknownprop_49f3cf70b605b44eb2822fe91c57bca94bae304f4b9278fa190485d2a33fdf59 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_57767f805436b599e99b8ac6663fa6b7758904d24620ff860a059bb817bebc7c with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.