proposition: Theorem Zpow_mod_Zpower_correct: forall a m n, 1 < n -> 0 <= m -> Zpow_mod a m n = (a ^ m) mod n.
proof: Proof. intros a m n; case m; simpl; auto. intros; apply Zpow_mod_pos_Zpower_pos_correct; auto with zarith. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic