diff --git a/theories/itv.v b/theories/itv.v
index e8ce672cb..e7ff196b4 100644
--- a/theories/itv.v
+++ b/theories/itv.v
@@ -880,3 +880,29 @@ Goal (x%:inum * y%:inum)%:i01 = x%:inum%:i01.
 Abort.
 
 End Test2.
+
+Section Test2'.
+
+Variable R : realDomainType.
+
+Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
+  (1 - ((1 - p%:inum)%:i01%:inum * (1 - q%:inum)%:i01%:inum))%:i01.
+
+Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
+Proof.
+apply/val_inj => /=.
+by rewrite subr0 mulr1 opprB addrCA subrr addr0.
+Qed.
+
+Reserved Notation "p .~" (format "p .~", at level 5).
+
+Definition onem (p : R) : R := 1 - p.
+Notation "p .~" := (onem p).
+
+Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
+  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
+
+Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
+  (1 - (p%:inum.~ * q%:inum.~))%:i01.
+
+End Test2'.