From 48ff7f0a13efa1dd107f398403224c0097a59a15 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sun, 10 Mar 2024 22:23:45 +0900 Subject: [PATCH] unnecessary parens --- lib/ssrR.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ssrR.v b/lib/ssrR.v index 411b4233..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)%coqR = (\sum_(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) :