The subproof is completed by applying OSNo_Quaternion_k.
The subproof is completed by applying OSNo_Octonion_i5.
The subproof is completed by applying OSNo_Octonion_i0.
Apply OSNo_mul_OSNo with
Quaternion_k,
Octonion_i5 leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.