proposition: Lemma im_conj (z : C) : z - z^* = 2%:R * (Im z)%:C * 'i.
proof: Proof. by rewrite ImJ_sub -!mulrA -expr2 sqr_i (mulrC _ (-1)) (mulrA _ (-1) _) mulrN1 opprB 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)