proposition: Lemma is_in_In : forall p lc, is_in p lc = true -> exists c, In c lc /\ p = nprim c.
proof: Proof. induction lc;simpl;try (intros;discriminate). intros;elimif. exists a;split;auto. inversion H0;trivial. destruct (IHlc H) as [c [H1 H2]];exists c;auto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod