proposition: Lemma re_conj (z : C) : 2%:R * (Re z)%:C = z + z^*.
proof: Proof. by rewrite ReJ_add mulrC mulfVK // pnatr_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)