We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li0i4: OSNo (i0 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i4 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i4) i5 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * k + - (0 ' * 1) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0L 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * 0 + 1 * k ' = (- k).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_1L (k ') (HSNo_conj_HSNo k HSNo_Quaternion_k) (from left to right).
We will prove 0 + k ' = (- k).
rewrite the current goal using conj_HSNo_k (from left to right).
We will prove 0 + - k = (- k).
An exact proof term for the current goal is add_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎