Add pow_Zpow to Util.ZUtil

I followed the naming scheme of things like div_Zdiv in the stdlib.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index a5716fca4..c6686b63c 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -65,6 +65,12 @@ Proof.
   rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
 Qed.
 
+Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n.
+Proof with auto using Zle_0_nat, Z.pow_nonneg.
+  intros; apply Z2Nat.inj...
+  rewrite <- pow_Z2N_Zpow, !Nat2Z.id...
+Qed.
+
 Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
   a ^ x mod m = 0.
 Proof.