proposition: Lemma normC_re_im : forall z : C, (normr z) ^+2 = ((Re z)^+2 + (Im z)^+2)%:C.
proof: Proof. case=> a b. rewrite sqr_normc /=. simpc. by rewrite -!expr2 mulrC -(addr0 (- (b * a) + b * a)) -addrA (@addKr R _ 0). 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)