proposition: Lemma allzprimeallpos : forall l : Zlist, allZPrime l -> allPos l.
proof: Proof. unfold allZPrime, allPos in |- *. simple induction l. simpl in |- *. intro. assumption. simpl in |- *. intros h t IH H. elim H. intros. elim H0. intros. split. apply Z.le_ge. apply Z.le_trans with 1%Z. unfold Z.le in |- *. simpl in |- *. discriminate. apply Zlt_le_weak. apply Z.gt_lt. assumption. apply IH. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list