proposition: Lemma Z_ggcd_coprime a b : let '(g, (a', b')) := Z.ggcd a b in g <> 0%coqZ -> coprime `|Z2int a'| `|Z2int b'|.
proof: Proof. move: (Z.ggcd_gcd a b) (Z.ggcd_correct_divisors a b). case (Z.ggcd _ _)=> g ab; case ab=> a' b' /= Hg [] Ha Hb Pg. rewrite /coprime; apply/eqP /Nat2Z.inj; rewrite -ZgcdE' /=. suff ->: a' = (a / g)%coqZ. { suff ->: b' = (b / g)%coqZ; [by apply Z.gcd_div_gcd|]. by rewrite Hb Z.mul_comm Z_div_mult_full. } by rewrite Ha Z.mul_comm Z_div_mult_full. 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)