proposition: Lemma Z_ggcd_1_r n : Z.ggcd n 1 = (1, (n, 1))%coqZ.
proof: Proof. move: (Z.ggcd_gcd n 1) (Z.ggcd_correct_divisors n 1); rewrite Z.gcd_1_r. case (Z.ggcd _ _)=> g ab /= ->; case ab=> a b []. by rewrite !Z.mul_1_l => <- <-. 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)