proposition: Lemma ZgcdE n d : Z.gcd n (Z.pos d) = Z.of_nat (div.gcdn `|Z2int n| (nat_of_pos d)).
proof: Proof. apply: Z.gcd_unique. { exact: Zle_0_nat. } { apply/Z.divide_abs_r; rewrite -Zabs2Nat.id_abs; apply/dvdnP. by rewrite Zabs_natE dvdn_gcdl. } { apply/Z.divide_abs_r; rewrite -Zabs2Nat.id_abs; apply/dvdnP. by rewrite Zabs_natE /= dvdn_gcdr. } move=> q Hn Hd; apply/Z.divide_abs_l; rewrite -Zabs2Nat.id_abs; apply/dvdnP. rewrite Zabs_natE dvdn_gcd. apply/andP; split; apply/dvdnP; rewrite -!Zabs_natE !Zabs2Nat.id_abs. { by apply/Z.divide_abs_l/Z.divide_abs_r. } { by apply/Z.divide_abs_l; rewrite -binnat.to_natE positive_nat_Z. } Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)