proposition: Lemma normc_re_im : forall z : C, (Normc.normc z) ^+2 = (Re z)^+2 + (Im z)^+2.
proof: Proof. case=> a b. rewrite -[x in (_ = x)]sqr_sqrtr // addr_ge0 //; by apply: sqr_ge0. 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)