Apply CD_mul_1R with
Sing 3,
CSNo,
minus_CSNo,
conj_CSNo,
add_CSNo,
mul_CSNo leaving 10 subgoals.
The subproof is completed by applying quaternion_tag_fresh.
The subproof is completed by applying CSNo_0.
The subproof is completed by applying CSNo_1.
The subproof is completed by applying minus_CSNo_0.
The subproof is completed by applying conj_CSNo_0.
The subproof is completed by applying conj_CSNo_1.
The subproof is completed by applying add_CSNo_0L.
The subproof is completed by applying add_CSNo_0R.
The subproof is completed by applying mul_CSNo_0L.
The subproof is completed by applying mul_CSNo_1R.