proposition: Lemma iter_Npow_mod_spec : forall n q p a, Z_of_N (iter_pos N (fun x : N => Npow_mod x q n) a p) = a^q^p mod n.
proof: Proof. induction p; mauto; intros; simpl Pos.iter; mauto; repeat rewrite IHp. rewrite (Zpower_mod ((a ^ q ^ p) ^ q ^ p));auto with zmisc. rewrite (Zpower_mod (a ^ q ^ p)); mauto. mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod