proposition: Lemma primezprime : forall n : nat, Prime n -> ZPrime (Z_of_nat n).
proof: Proof. unfold Prime, ZPrime in |- *. intros. elim H. intros. split. change (Z_of_nat n > Z_of_nat 1)%Z in |- *. apply Znat.inj_gt. assumption. intros. elim (H1 (Z.abs_nat q)). left. rewrite <- (inj_abs_pos q). rewrite H4. simpl in |- *. reflexivity. assumption. right. rewrite <- (inj_abs_pos q). rewrite H4. reflexivity. assumption. rewrite <- (abs_inj n). apply zdivdiv. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list