proposition: Lemma irreducible_poly_coprime (A : idomainType) (p q : {poly A}) : irreducible_poly p -> coprimep p q = ~~(p %| q)%R.
proof: Proof. case => H1 H2; apply/coprimepP/negP. move=> sPq H. by have := sPq p (dvdpp _) H; rewrite -size_poly_eq1; case: size H1 => [|[]]. move=> pNDq d dDp dPq. rewrite -size_poly_eq1; case: eqP => // /eqP /(H2 _) => /(_ dDp) dEp. by case: pNDq; rewrite -(eqp_dvdl _ dEp). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)