proposition: Lemma euclid_gcd (d1 d2 : nat) (x y q r : Z) : x = (q * y + r)%Z -> Zis_gcd x y (Z.of_nat d1) -> Zis_gcd r y (Z.of_nat d2) -> d1 = d2.
proof: Proof. intros H H0 H1 ; pose proof (euclid_gcd1 d1 x y q r H0 H) as H2. pose proof (Zis_gcd_unique r y _ _ H2 H1); lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow