Proofgold Proof

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