We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
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 Li6i1: OSNo (i6 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i1 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i1) 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 i6 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * i + - (0 ' * (- j)) = 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 i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (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 i6 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * 0 + (- j) * i ' = (- k).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j (- i) HSNo_Quaternion_j (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_j_i (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎