proposition: Lemma Im_invc : forall (z : C), Im z^-1 = (- Im z) / ((Re z) ^+ 2 + (Im z) ^+2).
proof: Proof. by case => a b; rewrite mulNr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)