proposition: Lemma gcdp_eq0 p q : gcdp p q == 0 = (p == 0) && (q == 0).
proof: Proof. apply/idP/idP; last by case/andP => /eqP -> /eqP ->; rewrite gcdp0. have h m n: gcdp m n == 0 -> (m == 0). by rewrite -(dvd0p m); move/eqP<-; rewrite dvdp_gcdl. by move=> ?; rewrite (h _ q) // (h _ p) // -eqp0 (eqp_ltrans (gcdpC _ _)) eqp0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)