Proofgold Proof

pf
Apply CD_add_assoc with Sing 3, CSNo, add_CSNo leaving 3 subgoals. The subproof is completed by applying quaternion_tag_fresh. The subproof is completed by applying CSNo_add_CSNo. The subproof is completed by applying add_CSNo_assoc. ■