From c5cb1ab2fe5fdfe17b3aa313965b863d883e8bf7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 24 Jan 2024 11:27:24 +0100
Subject: [PATCH] Strenghten In_size lemma

---
 utils/theories/MCList.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/utils/theories/MCList.v b/utils/theories/MCList.v
index 125f70869..c8cff4db1 100644
--- a/utils/theories/MCList.v
+++ b/utils/theories/MCList.v
@@ -1406,7 +1406,7 @@ Proof.
 Qed.
 
 Lemma In_size {A B} {x : A} {l : list A} (proj : A -> B) (size : B -> nat) :
-  In x l -> size (proj x) < S (list_size (size ∘ proj) l).
+  In x l -> size (proj x) < (list_size (size ∘ proj) l).
 Proof.
   induction l; cbn => //.
   intros [->|hin]. lia. specialize (IHl hin); lia.