proposition: Lemma prime_div_or_gcd1 : forall (p : nat) (a : Z), Prime p -> ZDivides (Z_of_nat p) a \/ gcd (Z_of_nat p) a 1.
proof: Proof. intros. elim (zdivdec a (Z_of_nat p)). left. assumption. right. unfold gcd in |- *. unfold common_div in |- *. split. split. split with p. simpl in |- *. rewrite <- plus_n_O. apply abs_inj. split with (Z.abs_nat a). simpl in |- *. apply plus_n_O. intros. elim H1. intros. rewrite abs_inj in H2. elim (primediv1p p e). intro. rewrite H4. apply le_n. intro. rewrite H4 in H3. elim H0. apply divzdiv. rewrite abs_inj. assumption. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd