diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-21 14:00:42 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-21 14:00:42 -0700 |
| commit | 9d6c6fea193320d2a97a2b676974e9e699c9ff93 (patch) | |
| tree | e224f7708482df0e2dc4244acd10fa7985b1a0ab /src | |
| parent | 002b5e36e5e3fdeb62deec7eea0a8b05c217c8ba (diff) | |
Another ZUtil lemma
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZUtil.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 00e227e2d..97bfd44a2 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1001,6 +1001,9 @@ Module Z. intros; autorewrite with zsimplify; lia. Qed. Hint Rewrite div_sub_small using lia : zsimplify. + + Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. + Proof. lia. Qed. End Z. Module Export BoundsTactics. |