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 Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li5i2: OSNo (i5 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i2 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i2) i3 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * j + - (0 ' * (- k)) = 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 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (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_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * 0 + (- k) * j ' = (- i).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR (- k) j (HSNo_minus_HSNo k HSNo_Quaternion_k) HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL k j HSNo_Quaternion_k HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_k_j (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i).
∎