proposition: Lemma poly_mul_creal_eq0_coprime p q x : coprimep p q -> p.[x] * q.[x] == 0 -> {p.[x] == 0} + {q.[x] == 0}.
proof: Proof. move=> /Bezout_eq1_coprimepP /sig_eqW [[u v] /= hpq]; pose_big_enough i. have := (erefl ((1 : {poly F}).[x i])). rewrite -{1}hpq /= hornerD hornerC. set upxi := (u * _).[_]. move=> hpqi. have [p_small|p_big] := lerP `|upxi| 2%:R^-1=> pqx0; [left|right]. move=> px0; apply: pqx0; apply: mul_creal_neq0=> //. apply: (@mul_neq0_creal v.[x]). apply: (@neq_crealP 2%:R^-1 i i); rewrite ?gtr0E //. rewrite /= subr0 -hornerM -(ler_add2l `|upxi|). rewrite (le_trans _ (ler_norm_add _ _)) // hpqi normr1. rewrite (monoLR (addrNK _) (ler_add2r _)). by rewrite {1}[1](splitf 2) /= mul1r addrK. move=> qx0; apply: pqx0; apply: mul_creal_neq0=> //. apply: (@mul_neq0_creal u.[x]). apply: (@neq_crealP 2%:R^-1 i i); rewrite ?gtr0E //. by rewrite /= subr0 -hornerM ltW. by close. 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)