Proofgold Proof

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