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

sum_list_with_in

parent 86e53498
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
theories/list_numbers.v
+ 2
− 0
View file @ 7cebbad3
...@@ -200,6 +200,8 @@ Section sum_list. ...@@ -200,6 +200,8 @@ 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) ls : x ∈ ls → f x ≤ sum_list_with f ls.
Proof. induction 1; simpl; lia. Qed.
Lemma join_reshape szs l : Lemma join_reshape szs l :
sum_list szs = length l → mjoin (reshape szs l) = l. sum_list szs = length l → mjoin (reshape szs l) = l.
Proof. Proof.
......
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