1 files changed, 38 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Z2Nat.v b/src/Util/ZUtil/Z2Nat.v
index d6dd49a41..75d27dcaf 100644
--- a/src/Util/ZUtil/Z2Nat.v
+++ b/src/Util/ZUtil/Z2Nat.v
@@ -7,3 +7,41 @@ Module Z2Nat.
     destruct n; try reflexivity; lia.
   Qed.
 End Z2Nat.
+
+Module Z.
+  Lemma pos_pow_nat_pos : forall x n,
+    Z.pos x ^ Z.of_nat n > 0.
+  Proof. intros; apply Z.lt_gt, Z.pow_pos_nonneg; lia. Qed.
+
+  Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
+                                   ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
+  Proof.
+    intros a n H; induction n as [|n IHn]; try reflexivity.
+    rewrite Nat2Z.inj_succ.
+    rewrite Nat.pow_succ_r by apply le_0_n.
+    rewrite Z.pow_succ_r by apply Zle_0_nat.
+    rewrite IHn.
+    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.
+  Hint Rewrite pow_Zpow : push_Zof_nat.
+  Hint Rewrite <- pow_Zpow : pull_Zof_nat.
+
+  Lemma Zpow_sub_1_nat_pow a v
+    : (Z.pos a^Z.of_nat v - 1 = Z.of_nat (Z.to_nat (Z.pos a)^v - 1))%Z.
+  Proof.
+    rewrite <- (Z2Nat.id (Z.pos a)) at 1 by lia.
+    change 2%Z with (Z.of_nat 2); change 1%Z with (Z.of_nat 1);
+      autorewrite with pull_Zof_nat.
+    rewrite Nat2Z.inj_sub
+      by (change 1%nat with (Z.to_nat (Z.pos a)^0)%nat; apply Nat.pow_le_mono_r; simpl; lia).
+    reflexivity.
+  Qed.
+  Hint Rewrite Zpow_sub_1_nat_pow : pull_Zof_nat.
+  Hint Rewrite <- Zpow_sub_1_nat_pow : push_Zof_nat.
+End Z.