Apply CD_add_minus_rinv with
Sing 3,
CSNo,
minus_CSNo,
add_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 add_CSNo_minus_CSNo_rinv.