proposition: Lemma fold_aux : forall a N l prod, (fold_left (fun (r : Z) (k : positive * positive) => r * (a ^(N / fst k) - 1) mod [|b|]) l (prod mod [|b|]) mod [|b|] = fold_left (fun (r : Z) (k : positive * positive) => r * (a^(N / fst k) - 1)) l prod mod [|b|])%Z.
proof: Proof. induction l;simpl;intros. rewrite Zmod_mod; auto with zarith. rewrite <- IHl; auto with zarith. rewrite Zmult_mod; auto with zarith. rewrite Zmod_mod; auto with zarith. rewrite <- Zmult_mod; auto with zarith. 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