proposition: Fact Op_gcdn_subproof n m : Z.of_nat (gcdn n m) = Z.gcd (Z.of_nat n) (Z.of_nat m).
proof: Proof. apply/esym/Z.gcd_unique; first by case: gcdn. - case/dvdnP: (dvdn_gcdl n m) => k {2}->; exists (Z.of_nat k); lia. - case/dvdnP: (dvdn_gcdr n m) => k {2}->; exists (Z.of_nat k); lia. - move=> k [n' Hkn] [m' Hkm]. suff/dvdnP [k' ->]: Z.abs_nat k %| gcdn n m. by apply/Znumtheory.Zdivide_Zabs_l; exists (Z.of_nat k'); lia. rewrite dvdn_gcd; apply/andP; split; apply/dvdnP; [exists (Z.abs_nat n') | exists (Z.abs_nat m')]; nia. Qed.
imports: Coq(ZArith ZifyClasses ZifyInst ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial)