diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-05 18:29:54 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-05 19:04:33 -0400 |
| commit | 8b99f9984343aa43b50c9ed722f159482930bdbe (patch) | |
| tree | 01c235cde89f8d5de8136a611a52bc5390d27d67 /src/Util/QUtil.v | |
| parent | 9faa549495539ace4347ba8627fbbf02a0cc0aa0 (diff) | |
Add pow_ceil_mul_nat_nonneg
Diffstat (limited to 'src/Util/QUtil.v')
| -rw-r--r-- | src/Util/QUtil.v | 11 |
1 files changed, 9 insertions, 2 deletions
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. |