proposition: Lemma allzprimeallprime : forall l : Zlist, allZPrime l -> allPrime (map _ _ Z.abs_nat l).
proof: Proof. unfold allPrime, allZPrime in |- *. simple induction l. simpl in |- *. intro. assumption. simpl in |- *. intros h t IH H. elim H. intros. split. apply zprimeprime. assumption. apply IH. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list