fix

math-comp · Oct 2, 2023 · ed13992 · ed13992
1 parent f676291
commit ed13992
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/hoelder.v b/theories/hoelder.v
@@ -310,7 +310,7 @@ have pq1 : p^-1 + q^-1 = 1.
 rewrite -(@powRr1 _ (w1 * x `^ p + w2 * y `^ p)); last first.
   by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// itv_ge0.
 have -> : 1 = p^-1 * p by rewrite mulVf ?gt_eqF.
-rewrite powRrM (gt0_ler_powR (le_trans _ (ltW p1)))//.
+rewrite powRrM (ge0_ler_powR (le_trans _ (ltW p1)))//.
 - by rewrite nnegrE addr_ge0// mulr_ge0 /w2 ?onem_ge0.
 - by rewrite nnegrE powR_ge0.
 have -> : w1 * x + w2 * y = w1 `^ (p^-1) * w1 `^ (q^-1) * x +