Proofgold Proof

pf
Apply CD_conj_CD with Sing 3, CSNo, minus_CSNo, conj_CSNo leaving 3 subgoals. The subproof is completed by applying quaternion_tag_fresh. The subproof is completed by applying CSNo_minus_CSNo. The subproof is completed by applying CSNo_conj_CSNo. ■