diff -r 953a47dc0519 -r feab36851df3 src/Provers/nat_transitive.ML
--- a/src/Provers/nat_transitive.ML	Tue Apr 08 10:48:42 1997 +0200
+++ b/src/Provers/nat_transitive.ML	Tue Apr 08 12:03:59 1997 +0200
@@ -178,7 +178,7 @@
 (* recognize and solve trivial goal *)
 fun triv_sol(x,i,y,j,_) =
   if x=y andalso i<j
-  then Some(Incr1(Incr2(Thm([],Less.lessI),i),j-i)) else
+  then Some(Incr1(Incr2(Thm([],Less.lessI),i),j-i-1)) else
   if Less.is_zero(x) andalso i<j
   then Some(Incr1(Incr2(Thm([],Less.zero_less_Suc),i),j-i-1))
   else None;