Apply CD_conj_minus with
Sing 3,
CSNo,
minus_CSNo,
conj_CSNo leaving 4 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.
The subproof is completed by applying conj_minus_CSNo.