diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-09 16:32:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-09 16:32:06 -0400 |
| commit | f7734b2d0f4dffb46c50fa89985b926377ec5e96 (patch) | |
| tree | 032bd1fa8866225552f48729fdff072ae2b5c4cf /src/Util/ZUtil.v | |
| parent | 810b026d3750fa882be7e3a81cc44a97484d1398 (diff) | |
Make replace_with_neg more powerful
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d905cc1f2..2f354ff1a 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2693,6 +2693,8 @@ Module Z. repeat match goal with | [ H : (-?x) < 0 |- _ ] => assert (0 < x) by omega; clear H | [ H : 0 > (-?x) |- _ ] => assert (0 < x) by omega; clear H + | [ H : (-?x) <= 0 |- _ ] => assert (0 <= x) by omega; clear H + | [ H : 0 >= (-?x) |- _ ] => assert (0 <= x) by omega; clear H | [ H : -?x <= -?y |- _ ] => apply Z.opp_le_mono in H | [ |- -?x <= -?y ] => apply Z.opp_le_mono | _ => progress rewrite <- Z.opp_le_mono in * @@ -2713,6 +2715,8 @@ Module Z. repeat match goal with | [ H : ?x < 0 |- _ ] => replace_with_neg x | [ H : 0 > ?x |- _ ] => replace_with_neg x + | [ H : ?x <= 0 |- _ ] => replace_with_neg x + | [ H : 0 >= ?x |- _ ] => replace_with_neg x end. Lemma shiftl_le_Proper2 y |