From ee75502025e9fb5b988b025521aabab6f849b2e9 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 11 Mar 2024 16:50:55 +0900 Subject: [PATCH] fix sumRE (#113) --- lib/ssrR.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ssrR.v b/lib/ssrR.v index c5c7d6fa..76104f8c 100644 --- a/lib/ssrR.v +++ b/lib/ssrR.v @@ -906,7 +906,7 @@ Section temporary_lemmas. Local Open Scope ring_scope. Lemma sumRE (I : Type) (r : seq I) (P : pred I) (F : I -> R) : - \sum_(i <- r | P i) F i = \big[+%R/0]_(i <- r | P i) F i. + (\sum_(i <- r | P i) F i)%coqR = \sum_(i <- r | P i) F i. Proof. by []. Qed. Lemma bigmaxRE (I : Type) (r : seq I) (P : pred I) (F : I -> R) :