proposition: Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n.
proof: Proof. unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; intros; mauto. rewrite IHl; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod