proposition: Lemma allprimeallzprime : forall l : natlist, allPrime l -> allZPrime (map _ _ Z_of_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 primezprime. assumption. apply IH. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list