proposition: Lemma pow_mod_spec : forall n a m, Z_of_N (pow_mod a m n) = a^m mod n.
proof: Proof. induction m; mauto; simpl; intros; mauto. rewrite Zmult_mod; auto with zmisc. rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. rewrite <- IHm; mauto. destruct (pow_mod a m n); mauto. rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. rewrite <- IHm. destruct (pow_mod a m n);simpl; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod