From 810b026d3750fa882be7e3a81cc44a97484d1398 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 9 Apr 2017 16:17:38 -0400 Subject: Handle more things in Z.peel_le --- src/Util/ZUtil.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/Util/ZUtil.v') 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. -- cgit v1.2.3