diff --git a/theories/normedtype.v b/theories/normedtype.v
index bf18d7bcd..ad227e6e1 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -244,11 +244,11 @@ Proof.
 apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
   exists (-%R @` A).
     exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
-    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+    by apply: reA; rewrite ?(@eqr_opp R)//= opprK addrC distrC.
   rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
   by rewrite opprK.
 exists e => //= x/=; rewrite -opprD normrN => axe xa.
-exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?(@eqr_oppLR R)//=.
 by rewrite opprK.
 Qed.
 
diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v
index dae60a5b9..ab1bd579a 100644
--- a/theories/showcase/summability.v
+++ b/theories/showcase/summability.v
@@ -36,7 +36,7 @@ by move=> A B /=; exists (A `|` B) => P /=; rewrite fsubUset => /andP[].
 Qed.
 
 Definition partial_sum {I : choiceType} {R : zmodType}
-  (x : I -> R) (A : {fset I}) : R := \sum_(i : A) x (val i).
+  (x : I -> R) (A : {fset I}) : R := (\sum_(i : A) x (val i)).
 
 Definition sum (I : choiceType) {K : numDomainType} {R : normedModType K}
    (x : I -> R) : R := lim (partial_sum x @ totally).