An exact proof term for the current goal is HSNo_mul_HSNo j j HSNo_Quaternion_j HSNo_Quaternion_j.

An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.

We will prove p0 (j ⨯ j) = p0 (:-: 1).

rewrite the current goal using mul_HSNo_proj0 j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).

rewrite the current goal using minus_HSNo_proj0 1 HSNo_1 (from left to right).

We will prove p0 j * p0 j + - p1 j ' * p1 j = - p0 1.

rewrite the current goal using HSNo_p0_j (from left to right).

rewrite the current goal using HSNo_p1_j (from left to right).

rewrite the current goal using CSNo_HSNo_proj0 1 CSNo_1 (from left to right).

We will prove 0 * 0 + - 1 ' * 1 = - 1.

rewrite the current goal using conj_CSNo_1 (from left to right).

rewrite the current goal using mul_CSNo_0L 0 CSNo_0 (from left to right).

rewrite the current goal using mul_CSNo_1L 1 CSNo_1 (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 (j ⨯ j) = p1 (:-: 1).

rewrite the current goal using mul_HSNo_proj1 j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).

rewrite the current goal using minus_HSNo_proj1 1 HSNo_1 (from left to right).

We will prove p1 j * p0 j + p1 j * p0 j ' = - 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 j * p0 j + p1 j * p0 j ' = 0.

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 + 1 * 0 ' = 0.

rewrite the current goal using conj_CSNo_0 (from left to right).

We will prove 1 * 0 + 1 * 0 = 0.

rewrite the current goal using mul_CSNo_0R 1 CSNo_1 (from left to right).

An exact proof term for the current goal is add_CSNo_0L 0 CSNo_0.