We prove the intermediate claim Lkk: HSNo (k ⨯ k).
An exact proof term for the current goal is HSNo_mul_HSNo k k HSNo_Quaternion_k HSNo_Quaternion_k.
We prove the intermediate claim Lm1: HSNo (:-: 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply HSNo_proj0proj1_split (k ⨯ k) (:-: 1) Lkk Lm1 to the current goal.
We will prove p0 (k ⨯ k) = p0 (:-: 1).
rewrite the current goal using mul_HSNo_proj0 k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj0 1 HSNo_1 (from left to right).
We will prove p0 k * p0 k + - p1 k ' * p1 k = - p0 1.
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 CSNo_HSNo_proj0 1 CSNo_1 (from left to right).
We will prove 0 * 0 + - i ' * i = - 1.
rewrite the current goal using mul_CSNo_0L 0 CSNo_0 (from left to right).
rewrite the current goal using conj_CSNo_i (from left to right).
We will prove 0 + - (- i) * i = - 1.
rewrite the current goal using minus_mul_CSNo_distrL (- i) i (CSNo_minus_CSNo i CSNo_Complex_i) CSNo_Complex_i (from right to left).
We will prove 0 + (- - i) * i = - 1.
rewrite the current goal using minus_CSNo_invol i CSNo_Complex_i (from left to right).
We will prove 0 + i * i = - 1.
rewrite the current goal using Complex_i_sqr (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_CSNo_0L (- 1) (CSNo_minus_CSNo 1 CSNo_1).
We will prove p1 (k ⨯ k) = p1 (:-: 1).
rewrite the current goal using mul_HSNo_proj1 k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj1 1 HSNo_1 (from left to right).
We will prove p1 k * p0 k + p1 k * p0 k ' = - p1 1.
rewrite the current goal using HSNo_p1_1 (from left to right).
rewrite the current goal using minus_CSNo_0 (from left to right).
We will prove p1 k * p0 k + p1 k * p0 k ' = 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).
We will prove i * 0 + i * 0 ' = 0.
rewrite the current goal using conj_CSNo_0 (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).
An exact proof term for the current goal is add_CSNo_0L 0 CSNo_0.
∎