proposition: Theorem Zpower_mod p q n : 0 < n -> (p^q) mod n = ((p mod n)^q) mod n.
proof: Proof. intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1]. - pattern q; apply natlike_ind; trivial. clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial. rewrite Z.mul_mod_idemp_l by lia. rewrite Z.mul_mod, Rec, <- Z.mul_mod by lia. reflexivity. - rewrite !Z.pow_neg_r; auto with zarith. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower