proposition: Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
proof: Proof. intros x y; exists (Z.gcd x y). split; [apply Zgcd_is_gcd | apply Z.gcd_nonneg]. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat