fix sumRE

lib/ssrR.v

@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import Reals.
 From mathcomp Require Import lra.
 From mathcomp Require Import Rstruct.
 
@@ -488,7 +488,7 @@
 Proof. by rewrite -{1}(addR0 x) ltR_add2l. Qed.
 
 Lemma subR_gt0 x y : (0 < y - x) <-> (x < y).
 Proof. by split; [exact: Rminus_gt_0_lt | exact: Rlt_Rminus]. Qed.
 Lemma subR_lt0 x y : (y - x < 0) <-> (y < x).
 Proof. by split; [exact: Rminus_lt | exact: Rlt_minus]. Qed.
 Lemma subR_ge0 x y : (0 <= y - x) <-> (x <= y).
@@ -906,7 +906,7 @@
 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) :