diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-13 18:22:04 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-13 18:22:13 -0400 |
commit | 4fe56998670f7ae292e7f14ba7f4ad98938176aa (patch) | |
tree | 65922724be1b45fd4170cab1d8293d4b27f9638d /src/Util | |
parent | 65d876ee94d2e8e637aae3646fb4145020adc2a0 (diff) |
Add pow_ceil_mul_nat_divide_upperbound
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/QUtil.v | 12 |
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. |