Proofgold Proof

pf
Apply octonion_I with 0, minus_HSNo Complex_i leaving 2 subgoals. The subproof is completed by applying quaternion_0. Apply quaternion_minus_HSNo with Complex_i. The subproof is completed by applying quaternion_i. ■