Apply CD_mul_F_eq with
Sing 3,
CSNo,
minus_CSNo,
conj_CSNo,
add_CSNo,
mul_CSNo leaving 8 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_conj_CSNo.
The subproof is completed by applying CSNo_mul_CSNo.
The subproof is completed by applying minus_CSNo_0.
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_0R.