proposition: Lemma coprimep_root p q x : coprimep p q -> root p x -> q.[x] != 0.
proof: Proof. case/Bezout_coprimepP=> [[u v] euv] px0. move/eqpP: euv => [[c1 c2]] /andP /= [c1n0 c2n0 e]. suffices: c1 * (v.[x] * q.[x]) != 0. by rewrite !mulf_eq0 !negb_or c1n0 /=; case/andP. have := f_equal (horner^~ x) e; rewrite /= !hornerZ hornerD. by rewrite !hornerM (eqP px0) mulr0 add0r hornerC mulr1; move->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)