Commit 1ab781af authored by Jan's avatar Jan
Browse files

included Robbert's suggestions

parent b1d1901f
Pipeline #48272 passed with stage
in 9 minutes and 28 seconds
......@@ -200,13 +200,10 @@ 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 l.
- contradict H. apply not_elem_of_nil.
- cbn. rewrite elem_of_cons in H. destruct H as [H | H].
+ simplify_eq. lia.
+ specialize (IHl H). lia.
intros H. induction H.
all: simpl; lia.
Qed.
Lemma join_reshape szs l :
sum_list szs = length l mjoin (reshape szs l) = l.
......
Supports Markdown
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