proposition: Lemma all_in_In : forall lc lp, all_in lc lp = true -> forall pq, In pq lp -> exists c, In c lc /\ fst pq = nprim c.
proof: Proof. induction lp;simpl. intros H pq HF;elim HF. intros;destruct a;elimif. destruct H0;auto. rewrite <- H0;simpl;apply is_in_In;trivial. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod