diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 20f844db03a3285b4dc9a7bc35d3a1eca6cf4c76..5b53076bb48f53f6cb1d9699bbdf19b2bc575096 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -187,7 +187,9 @@ class split =
             let open Qed.Logic in
             match Lang.F.repr e with
             | Leq(x,y) -> split_cmp "Split (comp.)" x y
-            | Lt(x,y)  -> split_cmp "Split (comp.)" x y
+            | Lt(x,y) ->
+                let x = if F.is_int x then F.(e_add x e_one) else x in
+                split_cmp "Split (comp.)" x y
             | Eq(x,y)  when not (is_prop x || is_prop y) ->
                 split_cmp "Split (eq.)" x y
             | Neq(x,y) when not (is_prop x || is_prop y) ->