proposition: Lemma algRpfactorR_mul_gt0 (x a b : algC) : x \is Num.real -> a \is Num.real -> b \is Num.real -> a <= b -> ((algCpfactor x).[a] * (algCpfactor x).[b] <= 0) = (a <= x <= b).
proof: Proof. move=> xR aR bR ab; rewrite !algCpfactorRE// !hornerXsubC. have [lt_xa|lt_ax|->]/= := real_ltgtP xR aR; last first. - by rewrite subrr mul0r lexx ab. - by rewrite nmulr_rle0 ?subr_lt0 ?subr_ge0. rewrite pmulr_rle0 ?subr_gt0// subr_le0. by apply: negbTE; rewrite -real_ltNge// (lt_le_trans lt_xa). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)