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