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