From c47f48268f15e202a28b556845f231b2038cb426 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 15 Dec 2017 20:47:27 -0500 Subject: Add pow_ceil_mul_nat_divide_nonzero --- src/Util/QUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/QUtil.v') 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. -- cgit v1.2.3