proposition: Theorem Zis_gcd_gcd: forall a b c : Z, 0 <= c -> Zis_gcd a b c -> Z.gcd a b = c.
proof: Proof. intros a b c H1 H2. case (Zis_gcd_uniqueness_apart_sign a b c (Z.gcd a b)); auto. - apply Zgcd_is_gcd; auto. - Z.le_elim H1. + generalize (Z.gcd_nonneg a b); auto with zarith. intros H3 H4; contradict H3. rewrite <- (Z.opp_involutive (Z.gcd a b)), <- H4. now apply Zlt_not_le, Z.opp_lt_mono; rewrite Z.opp_involutive. + subst. now case (Z.gcd a b). Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat