From b1d1901f3a4145b52a90863c1906a17c60d89ae1 Mon Sep 17 00:00:00 2001
From: Jan Menz <s9jamenz@stud.uni-saarland.de>
Date: Mon, 7 Jun 2021 11:04:47 +0200
Subject: [PATCH] explicitly named assumption
---
theories/list_numbers.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index c9a39d2d..28c37363 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -202,7 +202,7 @@ Section sum_list.
Qed.
Lemma sum_list_with_in x (f: A -> nat) l: x ∈ l -> f x ≤ sum_list_with f l.
Proof.
- intros. induction l.
+ 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.
--
GitLab