diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-09 16:17:38 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-09 16:17:38 -0400 |
commit | 810b026d3750fa882be7e3a81cc44a97484d1398 (patch) | |
tree | 2a4581995116c8356bcdda342696c7675110fd3e /src | |
parent | 2411beb5a789169a20d4ee348cc960911a0d2a0e (diff) |
Handle more things in Z.peel_le
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/ZUtil.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index f9f421686..d905cc1f2 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -325,6 +325,24 @@ Module Z. | [ |- _ * ?x <= _ * ?x ] => first [ apply Z.mul_le_mono_nonneg_r; [ zutil_arith | ] | apply Z.mul_le_mono_nonpos_r; [ zutil_arith | ] ] + | [ |- -_ <= -_ ] + => apply Z.opp_le_mono + | [ |- _ / ?x <= _ / ?x ] + => apply Z.div_le_mono; [ zutil_arith | ] + | [ |- ?x / _ <= ?x / _ ] + => apply Z.div_le_compat_l; [ zutil_arith | split; [ zutil_arith | ] ] + | [ |- Z.quot _ ?x <= Z.quot _ ?x ] + => apply Z.quot_le_mono; [ zutil_arith | ] + | [ |- Z.quot ?x _ <= Z.quot ?x _ ] + => apply Z.quot_le_compat_l; [ zutil_arith | split; [ zutil_arith | ] ] + | [ |- Z.max ?x _ <= Z.max ?x _ ] + => apply Z.max_le_compat_l + | [ |- Z.max _ ?x <= Z.max _ ?x ] + => apply Z.max_le_compat_r + | [ |- Z.min ?x _ <= Z.min ?x _ ] + => apply Z.min_le_compat_l + | [ |- Z.min _ ?x <= Z.min _ ?x ] + => apply Z.min_le_compat_r end. Ltac peel_le := repeat peel_le_step. |