proposition: Lemma gcdn_def d m n : d %| m -> d %| n -> (forall d', d' %| m -> d' %| n -> d' %| d) -> gcdn m n = d.
proof: Proof. move=> dv_dm dv_dn gdv_d; apply/eqP. by rewrite eqn_dvd dvdn_gcd dv_dm dv_dn gdv_d ?dvdn_gcdl ?dvdn_gcdr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)