Add pow_ceil_mul_nat_divide_upperbound

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v
index a3f4b1d00..71fdedeea 100644
--- a/src/Util/QUtil.v
+++ b/src/Util/QUtil.v
@@ -111,4 +111,16 @@ Section pow_ceil_mul_nat2.
     eapply Qfloor_resp_le.
     all: trivial; try omega; (eapply (Qle_trans _ 1 _); [vm_decide|assumption]).
   Qed.
+
+  Lemma pow_ceil_mul_nat_divide_upperbound i :
+    wt (S i) / (wt i) <= b^Qceiling f.
+  Proof.
+    rewrite pow_ceil_mul_S.
+    rewrite Z_div_mult_full; [|apply pow_ceil_mul_nat_nonzero].
+    all:[ > | omega | eapply (Qle_trans _ 1 _); [vm_decide|assumption].. ].
+    apply Z.pow_le_mono_r; [ assumption | ].
+    rewrite Z.le_sub_le_add_l, Z.add_comm.
+    etransitivity; [ | apply Qceiling_le_add ].
+    reflexivity.
+  Qed.
 End pow_ceil_mul_nat2.