Apply HSNo_proj0proj1_split (k '') (:-: k) (HSNo_conj_HSNo k HSNo_Quaternion_k) (HSNo_minus_HSNo k HSNo_Quaternion_k) to the current goal.
We will prove p0 (k '') = p0 (:-: k).
rewrite the current goal using conj_HSNo_proj0 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj0 k HSNo_Quaternion_k (from left to right).
We will prove p0 k ' = - p0 k.
rewrite the current goal using HSNo_p0_k (from left to right).
We will prove 0 ' = - 0.
rewrite the current goal using minus_CSNo_0 (from left to right).
An exact proof term for the current goal is conj_CSNo_id_SNo 0 SNo_0.
We will prove p1 (k '') = p1 (:-: k).
rewrite the current goal using conj_HSNo_proj1 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj1 k HSNo_Quaternion_k (from left to right).
We will prove - p1 k = - p1 k.
Use reflexivity.
∎