proposition: Theorem Zgcd_1_rel_prime : forall a b, Z.gcd a b = 1 <-> rel_prime a b.
proof: Proof. unfold rel_prime; intros a b; split; intro H. - rewrite <- H; apply Zgcd_is_gcd. - case (Zis_gcd_unique a b (Z.gcd a b) 1); auto. + apply Zgcd_is_gcd. + intros H2; absurd (0 <= Z.gcd a b); auto with zarith. * rewrite H2; red; auto. * generalize (Z.gcd_nonneg a b); auto with zarith. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat