From 7401225830cb7a7365aa90564b459b437a531b34 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 25 Jul 2024 10:24:29 +0900
Subject: [PATCH] pinsker

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

diff --git a/probability/pinsker.v b/probability/pinsker.v
index fb0885ba..46bc6ee3 100644
--- a/probability/pinsker.v
+++ b/probability/pinsker.v
@@ -538,7 +538,8 @@ Qed.
 
 Lemma Pinsker_inequality_weak : d(P , Q) <= sqrt (2 * D(P || Q)).
 Proof.
-rewrite -(sqrt_Rsqr (d(P , Q))); last exact/pos_var_dist.
+rewrite -(sqrt_Rsqr (d(P , Q))); last first.
+  exact/RleP/pos_var_dist.
 apply sqrt_le_1_alt.
 apply (@leR_pmul2l (/ 2)); first by apply invR_gt0; lra.
 apply (@leR_trans (D(P || Q))); last first.