diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
index 8145cf99..7be1bb00 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
@@ -71,7 +71,7 @@ crySimpStep prop =
         (K (Nat 0), _) -> Just (y :== zero)
         (K Inf, _)     -> Just PTrue
         (_, K Inf)     -> Just (x :== inf)
-        _              -> Just (x :== y :|| x :> y)
+        _              -> Just (x :== inf :|| x :+ one :> y)
 
     x :==: y ->
       case (x,y) of