From 870c929a187f06217244bdd6923c23cae0b8acb0 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 17 May 2023 13:41:13 +0900
Subject: [PATCH] fix

---
 theories/prob_lang.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/prob_lang.v b/theories/prob_lang.v
index 91a573f74e..b694e4ef45 100644
--- a/theories/prob_lang.v
+++ b/theories/prob_lang.v
@@ -879,9 +879,9 @@ Lemma bernoulli_andE t U :
 Proof.
 rewrite /bernoulli_and 3!letin_sample_bernoulli/= /mand/= muleDr//= -muleDl//.
 rewrite !muleA -addeA -muleDl// -!EFinM !onem1S/= -splitr mulr1.
-have -> : (1 / 2 * (1 / 2) = 1 / 4 :> R)%R by rewrite mulf_div mulr1// -natrM.
+have -> : (1 / 2 * (1 / 2) = 1 / 4%:R :> R)%R by rewrite mulf_div mulr1// -natrM.
 rewrite /bernoulli/= measure_addE/= /mscale/= -!EFinM; congr( _ + (_ * _)%:E).
-have -> : (1 / 2 = 2 / 4 :> R)%R.
+have -> : (1 / 2 = 2 / 4%:R :> R)%R.
   by apply/eqP; rewrite eqr_div// ?pnatr_eq0// mul1r -natrM.
 by rewrite onem1S// -mulrDl.
 Qed.