diff options
| -rw-r--r-- | src/Util/ZUtil/Tactics/PeelLe.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Tactics/PeelLe.v b/src/Util/ZUtil/Tactics/PeelLe.v index f299e0acd..11ae2f87d 100644 --- a/src/Util/ZUtil/Tactics/PeelLe.v +++ b/src/Util/ZUtil/Tactics/PeelLe.v @@ -33,7 +33,7 @@ Module Z. => first [ apply Z.mul_le_mono_nonneg_r; [ zutil_arith | ] | apply Z.mul_le_mono_nonpos_r; [ zutil_arith | ] ] | [ |- -_ <= -_ ] - => apply Z.opp_le_mono + => apply -> Z.opp_le_mono | [ |- _ / ?x <= _ / ?x ] => apply Z.div_le_mono; [ zutil_arith | ] | [ |- ?x / _ <= ?x / _ ] |