proposition: Lemma prime_rel_prime : forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
proof: Proof. intros p H a H0; constructor; auto with zarith; intros ? H1 H2. apply prime_divisors in H1; intuition; subst; auto with zarith. - absurd (p | a); auto with zarith. - absurd (p | a); intuition. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat