fact: Fixpoint all_pow_mod (prod a : N) (l:dec_prime) (n:positive) {struct l}: N*N := match l with | nil => (prod,a) | (q,_) :: l => let m := Npred_mod (fold_pow_mod a l n) n in all_pow_mod (times_mod prod m n) (Npow_mod a q n) l n end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod