Apply CD_mul_0L with
Sing 3,
CSNo,
minus_CSNo,
conj_CSNo,
add_CSNo,
mul_CSNo leaving 7 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 minus_CSNo_0.
Apply add_CSNo_0L with
0.
The subproof is completed by applying CSNo_0.
The subproof is completed by applying mul_CSNo_0L.
The subproof is completed by applying mul_CSNo_0R.