We will
prove p0 (k ⨯ i) = p0 j.
rewrite the current goal using
HSNo_p0_j (from left to right).
We will
prove p0 k * p0 i + - (p1 i ' * p1 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).
rewrite the current goal using
HSNo_p0_i (from left to right).
rewrite the current goal using
HSNo_p1_i (from left to right).
We will
prove 0 * i + - (0 ' * i) = 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
We will
prove 0 * i + - (0 * i) = 0.
rewrite the current goal using mul_CSNo_0L i CSNo_Complex_i (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_0R 0 CSNo_0.
We will
prove p1 (k ⨯ i) = p1 j.
rewrite the current goal using
HSNo_p1_j (from left to right).
We will
prove p1 i * p0 k + p1 k * p0 i ' = 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
HSNo_p0_i (from left to right).
rewrite the current goal using
HSNo_p1_i (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_distrR i i CSNo_Complex_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.
rewrite the current goal using minus_CSNo_invol 1 CSNo_1 (from left to right).
An exact proof term for the current goal is add_CSNo_0L 1 CSNo_1.