proposition: Lemma test_Certif_In_Prime : forall lc, test_Certif lc = true -> forall c, In c lc -> prime (nprim c).
proof: Proof. intros lc; elim lc; simpl; auto. intros _ c H; case H. intros a; case a; simpl; clear a lc. intros N p l Rec H c [H1 | H1]; subst; auto with arith. intros n p l; case (test_Certif l); auto with zarith. 2: intros; discriminate. intros H H1 c [H2 | H2]; subst; auto with arith. simpl nprim. generalize H1; clear H1. case_eq (gt2 p). 2: intros; discriminate. case p; clear p; try (intros; discriminate; fail). unfold gt2; intros p H1. match goal with H: (?X ?< ?Y) = true |- _ => generalize (is_lt_spec X Y); rewrite H; clear H; intros H end. unfold Mp; case_eq (2 ^ p -1); try (intros; discriminate; fail). intros p1 Hp1. case_eq (n ?= p1)%P; try rewrite <- Hp1. 2: intros; discriminate. intros H2. match goal with H: (?X ?= ?Y)%P = true |- _ => generalize (is_eq_eq _ _ H); clear H; intros H end. generalize (lucas_prime H1); rewrite Hp1; rewrite <- H2. case (lucas p); try (intros; discriminate; fail); auto. intros N a d p l H. generalize (test_pock_correct N a d p). case (test_pock N a d p); auto. 2: intros; discriminate. generalize (all_in_In l d). case (all_in l d). 2: intros; discriminate. intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto. apply H2; auto. intros k Hk. case H1 with (2 := Hk); auto. intros x (Hx1, Hx2); rewrite Hx2; auto. intros N a d l H. generalize (test_spock_correct N a d). case test_spock; auto. 2: intros; discriminate. generalize (all_in_In l d). case (all_in l d). 2: intros; discriminate. intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto. apply H2; auto. intros k Hk. case H1 with (2 := Hk); auto. intros x (Hx1, Hx2); rewrite Hx2; auto. intros N S l A B x y l1. generalize (all_in_In l1 l). generalize (ell_test_correct N S l A B x y). case ell_test. case all_in; auto. intros H1 H2 H3 H4 c [H5 | H5]; try subst c; simpl; auto. apply H1. intros p Hp; case (H2 (refl_equal true) p); auto. intros x1 (Hx1, Hx2); rewrite Hx2; auto. intros; discriminate. intros; discriminate. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) Pmod Mod_op W Lucas PocklingtonCertificat NEll Bits