proposition: Lemma fold_aux : forall a N (n:positive) l prod, fold_left (fun (r : Z) (k : positive * positive) => r * (a ^(N / fst k) - 1) mod n) l (prod mod n) mod n = fold_left (fun (r : Z) (k : positive * positive) => r * (a^(N / fst k) - 1)) l prod mod n.
proof: Proof. induction l;simpl;intros; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod