proposition: Lemma coprimep_rdiv_gcd p q : (p != 0) || (q != 0) -> coprimep (rdivp p (gcdp p q)) (rdivp q (gcdp p q)).
proof: Proof. move=> hpq. have gpq0: gcdp p q != 0 by rewrite gcdp_eq0 negb_and. rewrite -gcdp_eqp1 -(@eqp_mul2r _ (gcdp p q)) // mul1r. have: gcdp p q %| p by rewrite dvdp_gcdl. have: gcdp p q %| q by rewrite dvdp_gcdr. rewrite !dvdpE !rdvdp_eq eq_sym; move/eqP=> hq; rewrite eq_sym; move/eqP=> hp. rewrite (eqp_ltrans (mulp_gcdl _ _ _)) hq hp. 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.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)