proposition: Lemma coprimepPn p q : p != 0 -> reflect (exists d, (d %| gcdp p q) && ~~ (d %= 1)) (~~ coprimep p q).
proof: Proof. move=> p0; apply: (iffP idP). by rewrite -gcdp_eqp1=> ng1; exists (gcdp p q); rewrite dvdpp /=. case=> d /andP [dg]; apply: contra; rewrite -gcdp_eqp1=> g1. by move: dg; rewrite (eqp_dvdr _ g1) dvdp1 size_poly_eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)