Proofgold Proof

pf
Apply CD_minus_F_eq with Sing 3, CSNo, minus_CSNo leaving 3 subgoals. The subproof is completed by applying quaternion_tag_fresh. The subproof is completed by applying CSNo_0. The subproof is completed by applying minus_CSNo_0. ■