Let z and w be given.
Assume Hz Hw.
We prove the intermediate
claim Lzw:
CSNo (mult' z w).
An
exact proof term for the current goal is
CSNo_mul_CSNo z w Hz Hw.
We prove the intermediate
claim Lwz:
CSNo (mult' w z).
An
exact proof term for the current goal is
CSNo_mul_CSNo w z Hw Hz.
We prove the intermediate claim LRezR: SNo (Re z).
An
exact proof term for the current goal is
CSNo_ReR z Hz.
We prove the intermediate claim LRewR: SNo (Re w).
An
exact proof term for the current goal is
CSNo_ReR w Hw.
We prove the intermediate claim LImzR: SNo (Im z).
An
exact proof term for the current goal is
CSNo_ImR z Hz.
We prove the intermediate claim LImwR: SNo (Im w).
An
exact proof term for the current goal is
CSNo_ImR w Hw.
We will prove Re (mult' z w) = Re (mult' w z).
Use transitivity with
Re z * Re w + - (Im w * Im z), and
Re w * Re z + - (Im z * Im w).
An
exact proof term for the current goal is
mul_CSNo_CRe z w Hz Hw.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com (Re z) (Re w) LRezR LRewR.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com (Im w) (Im z) LImwR LImzR.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CRe w z Hw Hz.
We will prove Im (mult' z w) = Im (mult' w z).
Use transitivity with
Im w * Re z + Im z * Re w, and
Im z * Re w + Im w * Re z.
An
exact proof term for the current goal is
mul_CSNo_CIm z w Hz Hw.
An
exact proof term for the current goal is
add_SNo_com (Im w * Re z) (Im z * Re w) (SNo_mul_SNo (Im w) (Re z) LImwR LRezR) (SNo_mul_SNo (Im z) (Re w) LImzR LRewR).
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CIm w z Hw Hz.