proposition: Lemma gcd_bezout_nat: forall (x y d : nat), (x > 0)%nat -> Zis_gcd (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) -> Bezout (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) .
proof: Proof. intros x y d H H0; destruct (Zis_gcd_bezout (Z.of_nat x) (Z.of_nat y) (Z.of_nat d) H0) as [u v ?]; now exists u v. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow