proposition: Lemma algCpfactorCgt0 x y : x \isn't Num.real -> y \is Num.real -> (algCpfactor x).[y] > 0.
proof: Proof. move=> xNR yR; rewrite algCpfactorCE// hornerM !hornerXsubC. rewrite [x]algCrect conjC_rect ?Creal_Re ?Creal_Im// !opprD !addrA opprK. rewrite -subr_sqr exprMn sqrCi mulN1r opprK ltr_paddl//. - by rewrite real_exprn_even_ge0// ?rpredB// ?Creal_Re. by rewrite real_exprn_even_gt0 ?Creal_Im ?orTb//=; apply/eqP/Creal_ImP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)