proposition: Theorem Zpow_mod_correct a m n : n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.
proof: Proof. intros Hn. destruct m; simpl; trivial. - apply Zpow_mod_pos_correct; auto with zarith. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower