Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: CSNo x0.
Assume H1: CSNo x1.
Apply SNo_add_SNo with mul_SNo (CSNo_Re x0) (CSNo_Re x1), minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1)) leaving 2 subgoals.
Apply SNo_mul_SNo with CSNo_Re x0, CSNo_Re x1 leaving 2 subgoals.
Apply CSNo_ReR with x0.
The subproof is completed by applying H0.
Apply CSNo_ReR with x1.
The subproof is completed by applying H1.
Apply SNo_minus_SNo with mul_SNo (CSNo_Im x0) (CSNo_Im x1).
Apply SNo_mul_SNo with CSNo_Im x0, CSNo_Im x1 leaving 2 subgoals.
Apply CSNo_ImR with x0.
The subproof is completed by applying H0.
Apply CSNo_ImR with x1.
The subproof is completed by applying H1.