From 8b99f9984343aa43b50c9ed722f159482930bdbe Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 5 Oct 2017 18:29:54 -0400
Subject: Add pow_ceil_mul_nat_nonneg

---
 src/Util/QUtil.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'src/Util/QUtil.v')

diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v
index 96bf34c3b..a3f4b1d00 100644
--- a/src/Util/QUtil.v
+++ b/src/Util/QUtil.v
@@ -50,8 +50,15 @@ Section pow_ceil_mul_nat.
     eapply zero_le_ceil_mul_nat.
   Qed.
 
+  Lemma pow_ceil_mul_nat_nonneg (Hb : 0 <= b)
+    : forall i, 0 <= wt i.
+  Proof.
+    intros.
+    apply Z.pow_nonneg; assumption.
+  Qed.
+
   Lemma pow_ceil_mul_S i :
-    wt (S i) = 
+    wt (S i) =
     (b ^ (Qceiling (f + f * inject_Z (Z.of_nat i)) - Qceiling (f * inject_Z (Z.of_nat i))) * wt i).
   Proof.
     rewrite Nat2Z.inj_succ.
@@ -104,4 +111,4 @@ Section pow_ceil_mul_nat2.
     eapply Qfloor_resp_le.
     all: trivial; try omega; (eapply (Qle_trans _ 1 _); [vm_decide|assumption]).
   Qed.
-End pow_ceil_mul_nat2.
\ No newline at end of file
+End pow_ceil_mul_nat2.
-- 
cgit v1.2.3