proposition: Lemma ZgcdE' n m : Z.gcd n m = Z.of_nat (gcdn `|Z2int n| `|Z2int m|).
proof: Proof. case m. { rewrite Z.gcd_0_r {2}/absz {2}/Z2int /= gcdn0 -Zabs2Nat.id_abs; f_equal. rewrite /Z.abs_nat /absz /Z2int. case n=>// p; rewrite -!binnat.to_natE //. case (Pos.to_nat _); [by rewrite GRing.oppr0|move=> n']. by rewrite /GRing.opp /=. } { by move=> p; rewrite ZgcdE nat_of_pos_Z_to_pos. } by move=> p; rewrite -Z.gcd_opp_r /= ZgcdE abszN /absz. 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)