proposition: Lemma zprimeprime : forall n : Z, ZPrime n -> Prime (Z.abs_nat n).
proof: Proof. unfold ZPrime, Prime in |- *. intros. elim H. intros. split. change (Z.abs_nat n > Z.abs_nat 1) in |- *. apply gtzgt. apply Z.le_trans with 1%Z. unfold Z.le in |- *. simpl in |- *. discriminate. apply Zlt_le_weak. apply Z.gt_lt. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. assumption. intros. elim (H1 (Z_of_nat q)). left. rewrite <- (abs_inj q). rewrite H3. simpl in |- *. reflexivity. right. rewrite <- (abs_inj q). rewrite H3. reflexivity. apply nat_ge_0. apply divzdiv. rewrite abs_inj. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list