We prove the intermediate
claim Ljk:
HSNo (j ⨯ k).
We will
prove p0 (j ⨯ k) = p0 i.
rewrite the current goal using
HSNo_p0_i (from left to right).
We will
prove p0 j * p0 k + - (p1 k ' * p1 j) = i.
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
HSNo_p0_k (from left to right).
rewrite the current goal using
HSNo_p1_k (from left to right).
We will
prove 0 * 0 + - (i ' * 1) = i.
rewrite the current goal using mul_CSNo_0R 0 CSNo_0 (from left to right).
rewrite the current goal using
mul_CSNo_1R (i ') (CSNo_conj_CSNo i CSNo_Complex_i) (from left to right).
We will
prove 0 + - (i ') = i.
rewrite the current goal using conj_CSNo_i (from left to right).
We will
prove 0 + - - i = i.
rewrite the current goal using minus_CSNo_invol i CSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_CSNo_0L i CSNo_Complex_i.
We will
prove p1 (j ⨯ k) = p1 i.
rewrite the current goal using
HSNo_p1_i (from left to right).
We will
prove p1 k * p0 j + p1 j * p0 k ' = 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).
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 + 1 * 0 ' = 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
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_1 (from left to right).
An exact proof term for the current goal is add_CSNo_0R 0 CSNo_0.