From b0276f9a4231b7271f946d646d717c5e96f3166b 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 91a573f74..b694e4ef4 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.