proposition: Lemma coprimepP p q : reflect (forall d, d %| p -> d %| q -> d %= 1) (coprimep p q).
proof: Proof. rewrite /coprimep; apply: (iffP idP) => [/eqP hs d dvddp dvddq | h]. have/dvdp_eqp1: d %| gcdp p q by rewrite dvdp_gcd dvddp dvddq. by rewrite -size_poly_eq1 hs; exact. by rewrite size_poly_eq1; case/andP: (dvdp_gcdlr p q); apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)