Skip to content
Snippets Groups Projects

sum_list_with_in

Merged Jan requested to merge Quarkbeast/stdpp:master into master
All threads resolved!
+ 5
0
@@ -200,6 +200,11 @@ 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.
Proof.
intros H. induction H.
all: simpl; lia.
Qed.
Lemma join_reshape szs l :
sum_list szs = length l mjoin (reshape szs l) = l.
Proof.
Loading