fix sumRE (#113)

affeldt-aist · Mar 11, 2024 · ee75502 · ee75502
1 parent 15762a0
commit ee75502
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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) :