diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-15 20:47:27 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-15 20:47:27 -0500 |
| commit | c47f48268f15e202a28b556845f231b2038cb426 (patch) | |
| tree | 83b96e7e8afd7191b1a0cea4f02889347b012213 /src/Util/QUtil.v | |
| parent | 716f566c403324418c1943791aac17b4b237a43c (diff) | |
Add pow_ceil_mul_nat_divide_nonzero
Diffstat (limited to 'src/Util/QUtil.v')
| -rw-r--r-- | src/Util/QUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v index 71fdedeea..86dabd13e 100644 --- a/src/Util/QUtil.v +++ b/src/Util/QUtil.v @@ -112,6 +112,13 @@ Section pow_ceil_mul_nat2. all: trivial; try omega; (eapply (Qle_trans _ 1 _); [vm_decide|assumption]). Qed. + Lemma pow_ceil_mul_nat_divide_nonzero i : + wt (S i) / (wt i) <> 0. + Proof. + pose proof (pow_ceil_mul_nat_divide i). + lia. + Qed. + Lemma pow_ceil_mul_nat_divide_upperbound i : wt (S i) / (wt i) <= b^Qceiling f. Proof. |