proposition: Lemma coprimep_div_gcd p q : (p != 0) || (q != 0) -> coprimep (p %/ (gcdp p q)) (q %/ gcdp p q).
proof: Proof. rewrite -negb_and -gcdp_eq0 -gcdp_eqp1 => gpq0. rewrite -(@eqp_mul2r (gcdp p q)) // mul1r (eqp_ltrans (mulp_gcdl _ _ _)). have: gcdp p q %| p by rewrite dvdp_gcdl. have: gcdp p q %| q by rewrite dvdp_gcdr. rewrite !dvdp_eq => /eqP <- /eqP <-. have lcn0 k : (lead_coef (gcdp p q)) ^+ k != 0. by rewrite expf_neq0 ?lead_coef_eq0. by apply: eqp_gcd; rewrite ?eqp_scale. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)