proposition: Lemma poly_mul_creal_eq0 p q x : p.[x] * q.[x] == 0 -> {p.[x] == 0} + {q.[x] == 0}.
proof: Proof. move=> mul_px_qx_eq0. have [->|p_neq0] := altP (p =P 0); first by left; rewrite horner_cst_creal. have [->|q_neq0] := altP (q =P 0); first by right; rewrite horner_cst_creal. pose d := gcdp p q; pose p' := gdcop d p; pose q' := gdcop d q. have cop_q'_d': coprimep p' q'. rewrite /coprimep size_poly_eq1. apply: (@coprimepP _ p' d _). + by rewrite coprimep_gdco. + by rewrite dvdp_gcdl. rewrite dvdp_gcd (dvdp_trans (dvdp_gcdl _ _)) ?dvdp_gdco //. by rewrite (dvdp_trans (dvdp_gcdr _ _)) ?dvdp_gdco. suff : (p' * q').[x] * (d ^+ (size p + size q)).[x] == 0. case/poly_mul_creal_eq0_coprime. + by rewrite coprimep_expr // coprimepMl ?coprimep_gdco. + move=> p'q'x_eq0. have : p'.[x] * q'.[x] == 0 by rewrite -horner_crealM. case/poly_mul_creal_eq0_coprime=> // /dvdp_creal_eq0 hp'q'. by left; apply: hp'q'; rewrite dvdp_gdco. by right; apply: hp'q'; rewrite dvdp_gdco. move/root_poly_expn_creal. rewrite addn_gt0 lt0n size_poly_eq0 p_neq0=> /(_ isT) dx_eq0. by left; apply: dvdp_creal_eq0 dx_eq0; rewrite dvdp_gcdl. move: mul_px_qx_eq0; rewrite -!horner_crealM. rewrite exprD mulrAC mulrA -mulrA [_ ^+ _ * _]mulrC. apply: dvdp_creal_eq0; rewrite ?dvdp_mul // dvdp_gdcor //; by rewrite gcdp_eq0 negb_and p_neq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)