We prove the intermediate claim Lji: HSNo (j ⨯ i).
An exact proof term for the current goal is HSNo_mul_HSNo j i HSNo_Quaternion_j HSNo_Complex_i.
Apply HSNo_proj0proj1_split (j ⨯ i) (:-: k) Lji (HSNo_minus_HSNo k HSNo_Quaternion_k) to the current goal.
We will prove p0 (j ⨯ i) = p0 (:-: k).
rewrite the current goal using minus_HSNo_proj0 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using mul_HSNo_proj0 j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
We will prove p0 j * p0 i + - (p1 i ' * p1 j) = - 0.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
We will prove 0 * i + - (0 ' * 1) = - 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_CSNo_0L i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0L 1 CSNo_1 (from left to right).
We will prove 0 + - 0 = - 0.
An exact proof term for the current goal is add_CSNo_0L (- 0) (CSNo_minus_CSNo 0 CSNo_0).
We will prove p1 (j ⨯ i) = p1 (:-: k).
rewrite the current goal using minus_HSNo_proj1 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using mul_HSNo_proj1 j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
We will prove p1 i * p0 j + p1 j * p0 i ' = - i.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
We will prove 0 * 0 + 1 * i ' = - i.
rewrite the current goal using mul_CSNo_0R 0 CSNo_0 (from left to right).
rewrite the current goal using mul_CSNo_1L (i ') (CSNo_conj_CSNo i CSNo_Complex_i) (from left to right).
rewrite the current goal using conj_CSNo_i (from left to right).
We will prove 0 + - i = - i.
An exact proof term for the current goal is add_CSNo_0L (- i) (CSNo_minus_CSNo i CSNo_Complex_i).
∎