proposition: Lemma root_coprimep (p q : {poly F}): (forall x, root p x -> q.[x] != 0) -> coprimep p q.
proof: Proof. move=> Ncmn; rewrite -gcdp_eqp1 -size_poly_eq1; apply/closed_rootP. by case=> r; rewrite root_gcd !rootE=> /andP [/Ncmn/negPf->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)