proposition: Lemma algRpfactorRE (x : algC) (xR : x \is Num.real) : algRpfactor x = 'X - (in_algR xR)%:P.
proof: Proof. rewrite /algRpfactor; case: eqP xR => //= p1 p2. by rewrite (bool_irrelevance p1 p2). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)