proposition: Lemma gcdp_def d m n : d %| m -> d %| n -> (forall d', d' %| m -> d' %| n -> d' %| d) -> gcdp m n %= d.
proof: Proof. move=> dm dn h; rewrite /eqp dvdp_gcd dm dn !andbT. by apply: h; [apply: dvdp_gcdl | apply: dvdp_gcdr]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)