We prove the intermediate claim Lik: HSNo (i ⨯ k).
An exact proof term for the current goal is HSNo_mul_HSNo i k HSNo_Complex_i HSNo_Quaternion_k.
Apply HSNo_proj0proj1_split (i ⨯ k) (:-: j) Lik (HSNo_minus_HSNo j HSNo_Quaternion_j) to the current goal.
We will prove p0 (i ⨯ k) = p0 (:-: j).
rewrite the current goal using minus_HSNo_proj0 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using mul_HSNo_proj0 i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
We will prove p0 i * p0 k + - (p1 k ' * p1 i) = - 0.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove i * 0 + - (i ' * 0) = - 0.
rewrite the current goal using mul_CSNo_0R i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0R (i ') (CSNo_conj_CSNo i CSNo_Complex_i) (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 (i ⨯ k) = p1 (:-: j).
rewrite the current goal using minus_HSNo_proj1 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using mul_HSNo_proj1 i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
We will prove p1 k * p0 i + p1 i * p0 k ' = - 1.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove i * i + 0 * 0 ' = - 1.
rewrite the current goal using mul_CSNo_0L (0 ') (CSNo_conj_CSNo 0 CSNo_0) (from left to right).
rewrite the current goal using Complex_i_sqr (from left to right).
We will prove - 1 + 0 = - 1.
An exact proof term for the current goal is add_CSNo_0R (- 1) (CSNo_minus_CSNo 1 CSNo_1).
∎