proposition: Theorem rel_prime_1: forall n, rel_prime 1 n.
proof: Proof. intros n; red; apply Zis_gcd_intro; auto. - exists 1; reflexivity. - exists n; rewrite Z.mul_1_r; reflexivity. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat