diff options
author | Jason Gross <jagro@google.com> | 2016-07-21 14:07:08 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-21 14:07:08 -0700 |
commit | 57bd30d9c16ff44c0fb7b771bdb1fcd579f7b08d (patch) | |
tree | b60a8c0e671e7f2c7d85eb0a5195093798eded61 | |
parent | 9d6c6fea193320d2a97a2b676974e9e699c9ff93 (diff) |
Add another ZUtil lemma
-rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 97bfd44a2..d26859ecc 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1004,6 +1004,13 @@ Module Z. Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. Proof. lia. Qed. + + Lemma mul_div_lt_by_le x y z b : 0 <= y < z -> 0 <= x < b -> x * y / z < b. + Proof. + intros [? ?] [? ?]; eapply Z.le_lt_trans; [ | eassumption ]. + auto with zarith. + Qed. + Hint Resolve mul_div_lt_by_le : zarith. End Z. Module Export BoundsTactics. |