diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index a3fce30e976a3e40514f8360a44b64533fccd4ea..11c1bb1718860a0e0fdf3275dabbcffe1282bab2 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -200,7 +200,7 @@ Section sum_list.
   Proof.
     induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
   Qed.
-  Lemma sum_list_with_in x (f: A → nat) l: x ∈ l → f x ≤ sum_list_with f l.  
+  Lemma sum_list_with_in x (f : A → nat) l : x ∈ l → f x ≤ sum_list_with f l.
   Proof.
     intros H. induction H.
     all: simpl; lia.