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