proposition: Lemma coprimep_root (p q : {poly F}) x : coprimep p q -> p.[x] == 0 -> q.[x] != 0.
proof: Proof. move=> /Bezout_eq1_coprimepP /sig_eqW [[u v] hpq] px0. have upx_eq0 : u.[x] * p.[x] == 0 by rewrite px0 mul_creal0. pose_big_enough i. have := (erefl ((1 : {poly F}).[x i])). rewrite -{1}hpq /= hornerD hornerC. set upxi := (u * _).[_] => hpqi. apply: (@neq_crealP ((ubound v.[x])%CR^-1 / 2%:R) i i) => //. by rewrite pmulr_rgt0 ?gtr0E // ubound_gt0. rewrite /= subr0 ler_pdivr_mull ?ubound_gt0 //. apply: le_trans (_ : `|(v * q).[x i]| <= _); last first. by rewrite hornerM normrM ler_wpmul2r ?normr_ge0 ?(uboundP v.[x]). rewrite -(ler_add2l `|upxi|) (le_trans _ (ler_norm_add _ _)) // hpqi normr1. rewrite (monoLR (addrNK _) (ler_add2r _)). rewrite {1}[1](splitf 2) /= mul1r addrK ltW // /upxi hornerM. by rewrite (@eq0_modP _ upx_eq0) ?gtr0E. 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)