proposition: Lemma algRpfactorCE (x : algC) : x \isn't Num.real -> algRpfactor x = 'X^2 - (in_algR (Creal_Re x) *+ 2) *: 'X + ((in_algR (normr_real x))^+2)%:P.
proof: Proof. by rewrite /algRpfactor; case: eqP => // p; rewrite p. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)