proposition: Lemma algCpfactorE x : algCpfactor x = ('X - x%:P) * ('X - x^*%:P) ^+ (x \isn't Num.real).
proof: Proof. by have [/algCpfactorRE|/algCpfactorCE] := boolP (_ \is _); rewrite ?mulr1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)