Apply mul_OSNo_mul_HSNo with
Quaternion_k,
Quaternion_k,
λ x0 x1 . x1 = minus_OSNo 1 leaving 3 subgoals.
The subproof is completed by applying HSNo_Quaternion_k.
The subproof is completed by applying HSNo_Quaternion_k.
Apply minus_OSNo_minus_HSNo with
1,
λ x0 x1 . mul_HSNo Quaternion_k Quaternion_k = x1 leaving 2 subgoals.
The subproof is completed by applying HSNo_1.
The subproof is completed by applying Quaternion_k_sqr.