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 Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
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 Li3i4: OSNo (i3 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i4 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i4) i6 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (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 ' * (- i)) = 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 (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (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_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (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 + (- i) * k ' = (- j).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR (- i) k (HSNo_minus_HSNo i HSNo_Complex_i) HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_i_k (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j).
∎