More lemmas about complex numbers: Re and Im intertwining with * and ^*.

[SnarkBoojum]

Trying to play with trigonometry formulas, I found the following lemmas on complex numbers useful:

Lemma conjRe: forall z: CC, Re z^* = Re z.
Proof.
by move=> [a b].
Qed.

Lemma conjIm: forall z: CC, Im z^* = -Im z.
Proof.
by move=> [a b].
Qed.

Lemma mulRe: forall w z: CC, Re (w * z) = (Re w) * (Re z) - (Im w) * (Im z).
Proof.
by move=> [a b] [c d].
Qed.

Lemma mulIm: forall w z: CC, Im (w * z) = (Re w) * (Im z) + (Im w) * (Re z).
Proof.
by move=> [a b] [c d].
Qed.