proposition: Lemma test_Certif_In_Prime : forall lc, test_Certif lc = true -> forall c, In c lc -> prime (nprim c).
proof: Proof. Proof with mauto. induction lc;simpl;intros. elim H0. destruct H0. subst c;destruct a;simpl... elimif. CaseEq (Mp p);[intros Heq|intros N' Heq|intros N' Heq];rewrite Heq in H; try discriminate H. elimif. CaseEq (SS p);[intros Heq'|intros N'' Heq'|intros N'' Heq'];rewrite Heq' in H; try discriminate H. rewrite H2;rewrite <- Heq. apply LucasLehmer;trivial. (destruct p; try discriminate H1). simpl in H1; generalize (is_lt_spec 2 p); rewrite H1; auto. elimif. apply (test_pock_correct N a d p); mauto. intros k Hin;destruct (all_in_In _ _ H1 _ Hin) as (c,(H2,H3)). rewrite H3;auto. discriminate. discriminate. destruct a;elimif;auto. discriminate. discriminate. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod