proposition: Theorem Zpow_mod_pos_correct a m n : n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n.
proof: Proof. intros Hn. induction m as [m IHm|m IHm|]. - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag. rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r. rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial. rewrite <- IHm, <- Z.mul_mod by trivial. simpl. now destruct (Zpow_mod_pos a m n). - rewrite <- Pos.add_diag at 2. rewrite Zpower_pos_is_exp. rewrite Z.mul_mod by trivial. rewrite <- IHm. simpl. now destruct (Zpow_mod_pos a m n). - now rewrite Zpower_pos_1_r. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower