Proofgold Proof

pf
Apply OSNo_I with 0, minus_HSNo Quaternion_k leaving 2 subgoals. The subproof is completed by applying HSNo_0. Apply HSNo_minus_HSNo with Quaternion_k. The subproof is completed by applying HSNo_Quaternion_k. ■