proposition: Lemma algCpfactorRE (x : algC) : x \is Num.real -> algCpfactor x = 'X - x%:P.
proof: Proof. by move=> xR; rewrite algRpfactorRE map_polyXsubC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)