From 4fe56998670f7ae292e7f14ba7f4ad98938176aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 13 Oct 2017 18:22:04 -0400 Subject: Add pow_ceil_mul_nat_divide_upperbound --- src/Util/QUtil.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Util/QUtil.v') 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. -- cgit v1.2.3