From ca70a30c8734fc3438d3a4ea3054f57ea6e43844 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 21 Sep 2023 17:27:31 +0900
Subject: [PATCH] nitpick

---
 theories/hoelder.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/hoelder.v b/theories/hoelder.v
index 7ff1485764..4d958e0527 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -254,7 +254,8 @@ Local Open Scope ring_scope.
 Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) :
   0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 ->
   0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
-  a1 * b1 + a2 * b2 <= (a1`^p + a2`^p) `^ (p^-1) * (b1`^q + b2`^q)`^(q^-1).
+  a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
+                       (b1 `^ q + b2 `^ q) `^ q^-1.
 Proof.
 move=> a10 a20 b10 b20 p0 q0 pq.
 pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end.