Skip to content
Snippets Groups Projects
Commit 09d8a70f authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jan
Browse files

Robbert's changes to spaces

parent 1ab781af
No related branches found
No related tags found
No related merge requests found
Pipeline #48274 canceled
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/list_numbers.v
+ 1
− 1
View file @ 09d8a70f
...@@ -200,7 +200,7 @@ Section sum_list. ...@@ -200,7 +200,7 @@ Section sum_list.
Proof. Proof.
induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia. induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
Qed. 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. Proof.
intros H. induction H. intros H. induction H.
all: simpl; lia. all: simpl; lia.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment