diff --git a/builder/simplify_rules.h b/builder/simplify_rules.h
index b13a338f..7a4c981c 100644
--- a/builder/simplify_rules.h
+++ b/builder/simplify_rules.h
@@ -569,8 +569,7 @@ bool apply_less_rules(Fn&& apply) {
 
       apply(x%c0 < c1,
         true, eval(c0 > 0 && c0 <= c1),
-        false, eval(c0 > 0 && c1 <= 0),
-        x%c0 != c1, eval(c0 > 0 && c1 >= c0 - 1)) ||
+        false, eval(c0 > 0 && c1 <= 0)) ||
       apply(c0 < x%c1,
         true, eval(c1 > 0 && c0 < 0),
         false, eval(c1 > 0 && c0 >= c1 - 1),
@@ -669,14 +668,14 @@ bool apply_less_rules(Fn&& apply) {
       apply(x + z < max(x, y), z < max(y - x, 0), !is_constant(x)) ||
 
       apply(min(z, x + y) < x + w, min(y, z - x) < w, !is_constant(x)) ||
-      apply(min(z, x - y) < x + w, min(-y, z - x) < w, !is_constant(x)) ||
+      apply(min(z, x - y) < x + w, 0 < w + max(y, x - z), !is_constant(x)) ||
       apply(max(z, x + y) < x + w, max(y, z - x) < w, !is_constant(x)) ||
-      apply(max(z, x - y) < x + w, max(-y, z - x) < w, !is_constant(x)) ||
+      apply(max(z, x - y) < x + w, 0 < w + min(y, x - z), !is_constant(x)) ||
 
       apply(x + y < max(w, x + z), y < max(z, w - x), !is_constant(x)) ||
-      apply(x + y < max(w, x - z), y < max(-z, w - x), !is_constant(x)) ||
+      apply(x + y < max(w, x - z), y + min(z, x - w) < 0, !is_constant(x)) ||
       apply(x + y < min(w, x + z), y < min(z, w - x), !is_constant(x)) ||
-      apply(x + y < min(w, x - z), y < min(-z, w - x), !is_constant(x)) ||
+      apply(x + y < min(w, x - z), y + max(z, x - w) < 0, !is_constant(x)) ||
 
       // Selects
       apply(select(x, c0, y) < c1, select(x, eval(c0 < c1), y < c1)) ||
@@ -740,8 +739,6 @@ bool apply_equal_rules(Fn&& apply) {
     
       apply(select(x, y, z) == select(x, w, u), select(x, y == w, z == u)) ||
       apply(v + select(x, y, z) == select(x, w, u), select(x, w == v + y, u == v + z)) ||
-      apply(v - select(x, y, z) == select(x, w, u), select(x, w == v - y, u == v - z)) ||
-      apply(select(x, y, z) - v == select(x, w, u), select(x, w == y - v, u == z - v)) ||
       apply(select(x, c0, y) == c1, select(x, eval(c0 == c1), y == c1)) ||
       apply(select(x, y, c0) == c1, select(x, y == c1, eval(c0 == c1))) ||
       apply(y == select(x == y, x, z), x == y || y == z) ||
diff --git a/builder/test/simplify/simplify.cc b/builder/test/simplify/simplify.cc
index 6ecc7277..0859bd8e 100644
--- a/builder/test/simplify/simplify.cc
+++ b/builder/test/simplify/simplify.cc
@@ -155,7 +155,7 @@ TEST(simplify, basic) {
   ASSERT_THAT(simplify(0 <= x % 4), matches(true));
   ASSERT_THAT(simplify(4 <= x % 4), matches(false));
   ASSERT_THAT(simplify((y / 4) * 4 <= y - 4), matches(false));
-  ASSERT_THAT(simplify((y / 4) * 4 <= y - 3), matches(3 == y % 4));
+  ASSERT_THAT(simplify((y / 4) * 4 <= y - 3), matches(3 <= y % 4));
   ASSERT_THAT(simplify((y / 4) * 4 <= y - 1), matches(boolean(y % 4)));
   ASSERT_THAT(simplify((y / 4) * 4 <= y), matches(true));