Apply CD_conj_mul with
Sing 3,
CSNo,
minus_CSNo,
conj_CSNo,
add_CSNo,
mul_CSNo leaving 14 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 CSNo_add_CSNo.
The subproof is completed by applying CSNo_mul_CSNo.
The subproof is completed by applying minus_CSNo_invol.
The subproof is completed by applying conj_CSNo_invol.
The subproof is completed by applying conj_minus_CSNo.
The subproof is completed by applying conj_add_CSNo.
The subproof is completed by applying minus_add_CSNo.
The subproof is completed by applying add_CSNo_com.
The subproof is completed by applying conj_mul_CSNo.
The subproof is completed by applying minus_mul_CSNo_distrR.
The subproof is completed by applying minus_mul_CSNo_distrL.