fact: Fixpoint pow_mod_pred (a:w) (l:dec_prime) {struct l} : w := match l with | nil => a | (q, p)::l => if (p ?= 1) then pow_mod_pred a l else let a' := iter_pos _ (fun x => pow x q) a (Pos.pred p) in pow_mod_pred a' l end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) Pmod Mod_op W Lucas PocklingtonCertificat NEll