diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v
index 6b452592..65a37c29 100644
--- a/ecc_modern/ldpc_algo.v
+++ b/ecc_modern/ldpc_algo.v
@@ -203,7 +203,7 @@ Extract Constant Rmult => "( *.)".
 Extract Constant Rplus => "(+.)".
 Extract Constant Rinv  => "fun x -> 1. /. x".
 Extract Constant Ropp  => "(~-.)".
-(*Extraction "extraction/sumprod.ml" sumprod estimation.*)
+Extraction "extraction/sumprod.ml" sumprod estimation.
 
 Section ToGraph.
 
diff --git a/information_theory/channel_code.v b/information_theory/channel_code.v
index 965404a3..fc2ed823 100644
--- a/information_theory/channel_code.v
+++ b/information_theory/channel_code.v
@@ -73,7 +73,7 @@ Proof.
 rewrite /CodeErrRate div1R.
 apply/RleP/ (@leR_pmul2l (INR #|M|)); first exact/ltR0n.
 rewrite mulRA mulRV ?INR_eq0' -?lt0n // mul1R -iter_addR -big_const.
-by apply: leR_sumR => m _; exact: Pr_1.
+by apply: leR_sumR => m _; exact: Pr_le1.
 Qed.
 
 Definition scha (W : `Ch(A, B)) (c : code) := (1 - echa(W , c))%R.
diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v
index 2a567bfd..3198c51f 100644
--- a/information_theory/channel_coding_direct.v
+++ b/information_theory/channel_coding_direct.v
@@ -734,7 +734,7 @@ apply (@leR_ltR_trans
     move: (preimC_Cal_E epsilon0 i tb); by rewrite inE.
   apply (@leR_trans (Pr (W ``(| i ord0)) (~: Cal_E i ord0) +
     Pr (W ``(| i ord0)) (\bigcup_(i0 | i0 != ord0) (Cal_E i i0)))%R).
-    exact: Pr_union.
+    exact: le_Pr_setU.
   exact/leR_add2l/Pr_bigcup.
 rewrite first_summand //.
 set lhs := (\sum_(_ < _ | _) _)%R.
@@ -756,7 +756,7 @@ rewrite card_ord /=.
 apply (@leR_ltR_trans (epsilon0 + k%:R *
    Pr P `^ n `x (`O(P , W)) `^ n [set x | prod_rV x \in `JTS P W n epsilon0])%R).
   apply leR_add2r.
-  rewrite Pr_of_cplt leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //.
+  rewrite Pr_setC leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //.
   by case: Hepsilon0.
   by case: Hn => _ [_ []].
 apply (@leR_ltR_trans (epsilon0 +
diff --git a/information_theory/entropy.v b/information_theory/entropy.v
index 6f4a9aba..f55bde35 100644
--- a/information_theory/entropy.v
+++ b/information_theory/entropy.v
@@ -490,8 +490,8 @@ rewrite fdistXE fdist_proj13E big_distrl /= -big_split; apply eq_bigr => b _ /=.
 rewrite !(fdistXE,fdistAE,fdistC12E) /= -mulRDr.
 have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R.
 rewrite -logM; last 2 first.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1 fdistAE /= fdistC12E.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1 fdistAE /= fdistC12E.
 congr (_ * log _).
 by rewrite -setX1 product_ruleC !setX1 mulRC.
 Qed.
@@ -570,7 +570,7 @@ transitivity (- (\sum_(a in A) \sum_(b in B) PQ (a, b) * log (P a)) +
   rewrite addRC -mulRN -mulRDr addR_opp.
   have [->|H0] := eqVneq (PQ (a, b)) 0; first by rewrite !mul0R.
   congr (_ * _); rewrite logDiv //.
-  - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1.
+  - by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1.
   - by apply/RltP; rewrite -fdist_gt0; exact: dom_by_fdist_fstN H0.
 rewrite -subR_opp; congr (_ - _).
 - rewrite /entropy; congr (- _); apply/eq_bigr => a _.
@@ -759,12 +759,12 @@ rewrite fdistXE fdistAE /= -mulRN -mulRDr.
 have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R.
 congr (_ * _).
 rewrite addRC addR_opp -logDiv; last 2 first.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdistA_dominN H0.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdistA_dominN H0.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0.
 congr (log _).
 rewrite divRM; last 2 first.
-  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0.
-  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj23_dominN H0.
+  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0.
+  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj23_dominN H0.
 rewrite {2}/Rdiv -mulRA mulRCA {1}/Rdiv [in LHS]mulRC; congr (_ * _).
 rewrite -[in X in _ = X * _]setX1 jproduct_rule_cond setX1 -mulRA mulRV ?mulR1 //.
 rewrite /jcPr divR_neq0' // ?setX1 !Pr_set1.
diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v
index 024b1ae8..eb0aa812 100644
--- a/information_theory/joint_typ_seq.v
+++ b/information_theory/joint_typ_seq.v
@@ -130,7 +130,7 @@ have : (JTS_1_bound <= n)%nat ->
     have : 1 <= 3 by lra.
     move/(set_typ_seq_incl P m (ltRW He)) => Hincl.
     rewrite (Pr_DMC_fst P W (fun x => x \notin `TS P m epsilon)).
-    apply/Pr_incl/subsetP => i /=; rewrite !inE.
+    apply/subset_Pr/subsetP => i /=; rewrite !inE.
     apply contra.
     by move/subsetP : Hincl => /(_ i); rewrite !inE.
   have {H1}HnP : forall n, ('| up (aep_bound P (epsilon / 3)) | <= n)%nat ->
@@ -159,7 +159,7 @@ have : (JTS_1_bound <= n)%nat ->
     have : 1 <= 3 by lra.
     move/(set_typ_seq_incl (`O(P , W)) m (ltRW He)) => Hincl.
     rewrite Pr_DMC_out.
-    apply/Pr_incl/subsetP => i /=; rewrite !inE.
+    apply/subset_Pr/subsetP => i /=; rewrite !inE.
     apply contra.
     move/subsetP : Hincl => /(_ i).
     by rewrite !inE.
@@ -187,7 +187,7 @@ have : (JTS_1_bound <= n)%nat ->
     Pr (((P `X W) ) `^ m) (~: `TS ((P `X W)) m (epsilon / 3)).
     have : 1 <= 3 by lra.
     move/(set_typ_seq_incl ((P `X W)) m (ltRW He)) => Hincl.
-    apply/Pr_incl/subsetP => /= v; rewrite !inE.
+    apply/subset_Pr/subsetP => /= v; rewrite !inE.
     apply contra.
     by move/subsetP : Hincl => /(_ v); by rewrite !inE.
   have {H1}HnP_W m : ('| up (aep_bound ((P `X W)) (epsilon / 3)) | <= m)%nat ->
@@ -229,8 +229,8 @@ apply (@leR_trans (
  Pr ((P `X W) `^ n) [set x | (rV_prod x).1 \notin `TS P n epsilon] +
  Pr ((P `X W) `^ n) ([set x | ((rV_prod x).2 \notin `TS (`O( P , W)) n epsilon)] :|:
                       (~: `TS ((P `X W)) n epsilon)))).
-  exact: Pr_union.
-rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (Pr_union _ _ _).
+  exact: le_Pr_setU.
+rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (le_Pr_setU _ _ _).
 by apply/Req_le; congr Pr; apply/setP => t; rewrite !inE rV_prodK.
 Qed.
 
diff --git a/information_theory/jtypes.v b/information_theory/jtypes.v
index 1ed16f3d..2207417f 100644
--- a/information_theory/jtypes.v
+++ b/information_theory/jtypes.v
@@ -252,13 +252,13 @@ by move=> a b; rewrite ffunE.
 Defined.
 
 Definition jtype_enum A B n := pmap (@jtype_enum_f A B n)
-  (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat}]).
+  (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat})).
 
 Lemma jtype_enumP A B n : Finite.axiom (@jtype_enum A B n).
 Proof.
 case=> d f Hf H /=.
-have : Finite.axiom (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}}  |
-    (\sum_(a in A) \sum_(b in B) f a b == n)%nat }]).
+have : Finite.axiom (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}}  |
+    (\sum_(a in A) \sum_(b in B) f a b == n)%nat })).
   rewrite enumT; by apply enumP.
 move/(_ (@exist _ _ f Hf)) => <-.
 rewrite /jtype_enum /=.
@@ -291,8 +291,8 @@ eq_ind_r
                                               else
                                                 (sval f a b)%:R /
                                                     (\sum_(b0 in B) (sval f a) b0)%:R)*) |}
-                     ) (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} |
-                                           (\sum_(a in A) \sum_(b in B) f a b)%nat == n}]).
+                     ) (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} |
+                                           (\sum_(a in A) \sum_(b in B) f a b)%nat == n})).
   apply: eq_pmap => V.
   destruct Sumbool.sumbool_of_bool; last by rewrite Anot0 in e.
   destruct Sumbool.sumbool_of_bool; last by rewrite Bnot0 in e0.
@@ -357,13 +357,13 @@ move=> Anot0 Bnot0.
 move: (Anot0); case/card_gt0P => a _.
 move: (Bnot0); case/card_gt0P => b _.
 apply/card_gt0P.
-have [tmp Htmp] : [finType of {f : {ffun A -> {ffun B -> 'I_n.+1}} |
-                     \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}].
+have [tmp Htmp] : {f : {ffun A -> {ffun B -> 'I_n.+1}} |
+                     \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}.
   exists [ffun a1 => [ffun b1 => if (a1, b1) == (a, b) then
     Ordinal (ltnSn n) else Ordinal (ltn0Sn n)]].
   rewrite pair_big /=.
   rewrite (bigD1 (a, b)) //= big1 ; first by rewrite 2!ffunE eqxx addn0.
-  move=> p /negbTE Hp ; by rewrite 2!ffunE -surjective_pairing Hp.
+  by move=> p /negbTE Hp ; rewrite 2!ffunE -surjective_pairing Hp.
 have Htmp' : (forall a b,
         (chan_of_jtype Anot0 Bnot0 tmp) a b =
         (let ln := \sum_(b0 in B) (tmp a) b0 in
diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v
index 371d8754..3d82477f 100644
--- a/information_theory/source_coding_vl_converse.v
+++ b/information_theory/source_coding_vl_converse.v
@@ -689,9 +689,9 @@ Proof.
 pose m' := m.-1.
 have mpos : m = m'.+1.
   rewrite prednK // -ltR_nat ltR_neqAle; split => //; exact/leR0n.
-have: (@extension [finType of 'rV[A]_n] _ f) \o
+have: (@extension 'rV[A]_n _ f) \o
       (flatten \o map (fun x => @tval m _ (tuple_of_row x))) =1
-      @extension [finType of {: 'rV[ 'rV[A]_n ]_m} ] _ fm.
+      @extension {: 'rV[ 'rV[A]_n ]_m} _ fm.
    by elim => //= ta sta; rewrite /extension /= map_cat flatten_cat => <-.
 apply: eq_inj.
 apply: inj_comp => //.
diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v
index 384cf5e5..549618c8 100644
--- a/information_theory/typ_seq.v
+++ b/information_theory/typ_seq.v
@@ -237,7 +237,7 @@ Lemma TS_inf : aep_bound P epsilon <= n.+1%:R ->
 Proof.
 move=> k0_k.
 have H1 : (1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon) <= 1)%mcR.
-  by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_1].
+  by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_le1].
 have H2 : (forall x, x \in `TS P n.+1 epsilon ->
     exp2 (- n.+1%:R * (`H P + epsilon)) <=
     P `^ n.+1 x <= exp2 (- n.+1%:R * (`H P - epsilon)))%mcR.
diff --git a/information_theory/types.v b/information_theory/types.v
index 861e1f0f..cc459edb 100644
--- a/information_theory/types.v
+++ b/information_theory/types.v
@@ -473,10 +473,11 @@ case/boolP : [exists x, x \in T_{P}] => x_T_P.
   rewrite -(row_of_tupleK ta) in Hta.
   rewrite -(tuple_dist_type_entropy Hta).
   rewrite [X in X <= _](_ : _ = Pr (type.d P) `^ n (@row_of_tuple A n @: T_{P})).
-    by apply Pr_1.
+    exact: Pr_le1.
   symmetry.
   rewrite /Pr.
-  transitivity (\sum_(a| (a \in [finType of 'rV[A]_n]) && [pred x in (@row_of_tuple A n @: T_{P})] a)
+  transitivity (\sum_(a | (a \in [finType of 'rV[A]_n]) &&
+                          [pred x in (@row_of_tuple A n @: T_{P})] a)
       exp2 (- INR n * `H P)).
     apply eq_big => // ta'/= Hta'.
     rewrite -(@tuple_dist_type_entropy ta') //.
diff --git a/probability/bayes.v b/probability/bayes.v
index 4d79586e..ab45adc1 100644
--- a/probability/bayes.v
+++ b/probability/bayes.v
@@ -421,10 +421,10 @@ split.
       case ac: (a == c).
         rewrite -(eqP ac); exact.
       move=> _ _ _.
-      rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+      rewrite (proj2 (cPr_eq0P _ _ _)); last first.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ac.
-      rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+      rewrite (proj2 (cPr_eq0P _ _ _)); last first.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /= /eqP ->; rewrite ac.
       by rewrite mul0R.
@@ -441,7 +441,7 @@ split.
       set x := (X in X = X * X).
       move/Rxx2 => [] Hx.
         rewrite -/x Hx.
-        rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //.
+        rewrite (proj2 (cPr_eq0P _ _ _)) ?mul0R //.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ab.
       rewrite /cPr.
@@ -459,17 +459,17 @@ split.
       move/eqP in Hden.
       rewrite /cPr /Rdiv -mulRA mulVR // mulR1 mul1R.
       move/(f_equal (Rminus den)).
-      rewrite subRR setIC -Pr_diff => /Pr_set0P/(_ u).
-      rewrite !inE (eqP Hi) Hk eq_sym ab; exact.
+      rewrite subRR setIC -Pr_setD => /Pr_set0P/(_ u).
+      by rewrite !inE (eqP Hi) Hk eq_sym ab; exact.
     case: (ord_eq_dec k j).
       move=> <- {j} ik b.
       case bc: (b == c).
         rewrite (eqP bc); exact.
       move=> _ _ _.
-      rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+      rewrite (proj2 (cPr_eq0P _ _ _)); last first.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /andP [] _ /= /eqP ->; rewrite bc.
-      rewrite mulRC (proj2 (cPr_eq0 _ _ _)) ?mul0R //.
+      rewrite mulRC (proj2 (cPr_eq0P _ _ _)) ?mul0R //.
       by apply/Pr_set0P => u; rewrite !inE => /andP [] /= /eqP ->; rewrite bc.
     move=> nkj nij b HG Hvals; apply: HG => //.
     by rewrite Hvals set_val_tl // set_val_tl // set_val_hd.
@@ -631,10 +631,10 @@ case /boolP: [forall i in (e :&: g), _].
 rewrite negb_forall => /existsP [i].
 rewrite inE negb_imply => /andP [] /andP [Hie Hig] /eqP Hvi.
 right; rewrite /cinde_events.
-rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+rewrite (proj2 (cPr_eq0P _ _ _)); last first.
   apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi.
   case/andP: Hprod => /andP[] /eqP <- _ /eqP <-; exact: prod_vars_inter.
-rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //.
+rewrite (proj2 (cPr_eq0P _ _ _)) ?mul0R //.
 apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi.
 case/andP: Hprod => /eqP <- /eqP <-; exact: prod_vars_inter.
 Qed.
@@ -664,7 +664,7 @@ rewrite (proj2 (Pr_set0P _ _)); last first.
 suff : `Pr_P[finset (prod_vars f @^-1 B) | finset (prod_vars g @^-1 C)] = 0.
   by rewrite /cPr => ->; rewrite mulR0 div0R.
 (* prove incompatibility between B and C *)
-apply/cPr_eq0/Pr_set0P => u.
+apply/cPr_eq0P/Pr_set0P => u.
 rewrite !inE => /andP [] /eqP HB /eqP HC.
 move: Hnum; rewrite /den.
 have -> : g = (e :&: f :|: g) :\: ((e :&: f) :\: g).
@@ -745,7 +745,7 @@ split.
   rewrite negb_imply /vals => /andP [Hif].
   case /boolP: (i \in g) => Hig.
     (* B and C are incompatible *)
-    move: (Hfg i); by rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->.
+    by move: (Hfg i); rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->.
   case /boolP: (i \in e) => Hie;
     last by rewrite set_vals_tl // set_vals_tl // eqxx.
   (* A and B are incompatible *)
@@ -756,7 +756,7 @@ split.
   rewrite {1}/cinde_events -!preim_vars_inter setUid /=.
   case/Rxx2.
     (* cPr = 0 *)
-    move/cPr_eq0/Pr_set0P => Hx.
+    move/cPr_eq0P/Pr_set0P => Hx.
     have HAC :
       Pr P (finset (prod_vars e @^-1 A) :&: finset (prod_vars g @^-1 C)) = 0.
       apply Pr_set0P => u Hu; apply Hx.
@@ -767,8 +767,8 @@ split.
         by rewrite set_vals_prod_vars.
       case/boolP: (j \in e) => // je.
       by rewrite set_vals_tl // set_vals_prod_vars.
-    rewrite /cinde_events (proj2 (cPr_eq0 _ _ _)).
-      by rewrite (proj2 (cPr_eq0 _ _ _)) // mul0R.
+    rewrite /cinde_events (proj2 (cPr_eq0P _ _ _)).
+      by rewrite (proj2 (cPr_eq0P _ _ _)) // mul0R.
     apply/Pr_set0P => u Hu.
     apply(proj1 (Pr_set0P _ _) HAC).
     move: Hu; by rewrite !inE => /andP[] /andP[] -> _ ->.
diff --git a/probability/jfdist_cond.v b/probability/jfdist_cond.v
index c41cb4e4..b3a4eee7 100644
--- a/probability/jfdist_cond.v
+++ b/probability/jfdist_cond.v
@@ -20,7 +20,7 @@ Require Import fdist proba.
 (*      jfdist_cond PQ a == The conditional distribution derived from PQ      *)
 (*                          given a; same as fdist_cond0 when                 *)
 (*                          fdist_fst PQ a != 0.                              *)
-(*           PQ `(| a |) == notation jfdist_cond PQ a                         *)
+(*            PQ `(| a ) == notation jfdist_cond PQ a                         *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -59,10 +59,10 @@ Lemma jcPr_ge0 E F : 0 <= \Pr_[E | F].
 Proof. by rewrite jcPrE. Qed.
 
 Lemma jcPr_le1 E F : \Pr_[E | F] <= 1.
-Proof. by rewrite jcPrE; exact: cPr_max. Qed.
+Proof. by rewrite jcPrE; exact: cPr_le1. Qed.
 
 Lemma jcPr_gt0 E F : 0 < \Pr_[E | F] <-> \Pr_[E | F] != 0.
-Proof. by rewrite !jcPrE; apply cPr_gt0. Qed.
+Proof. by rewrite !jcPrE; apply cPr_gt0P. Qed.
 
 Lemma Pr_jcPr_gt0 E F : 0 < Pr P (E `* F) <-> 0 < \Pr_[E | F].
 Proof.
@@ -73,11 +73,13 @@ split.
   by apply/Pr_cPr_gt0; move: H; rewrite jcPrE -setTE -EsetT.
 Qed.
 
+(* TODO: rename *)
 Lemma jcPr_cplt E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F].
 Proof.
 by move=> PF0; rewrite 2!jcPrE EsetT setCX cPr_cplt ?EsetT // setTE Pr_setTX.
 Qed.
 
+(* TODO: rename *)
 Lemma jcPr_diff E1 E2 F : \Pr_[E1 :\: E2 | F] = \Pr_[E1 | F] - \Pr_[E1 :&: E2 | F].
 Proof.
 rewrite jcPrE DsetT cPr_diff jcPrE; congr (_ - _).
diff --git a/probability/proba.v b/probability/proba.v
index 0e17c035..8d89a9a3 100644
--- a/probability/proba.v
+++ b/probability/proba.v
@@ -1328,7 +1328,7 @@ Lemma cPr_ge0 E F : 0 <= `Pr_[E | F].
 Proof.
 rewrite /cPr; have [PF0|PF0] := eqVneq (Pr d F) 0.
   by rewrite setIC (Pr_domin_setI _ PF0) div0R.
-by apply divR_ge0 => //; rewrite Pr_gt0.
+by apply divR_ge0 => //; rewrite Pr_gt0P.
 Qed.
 Local Hint Resolve cPr_ge0 : core.
 
@@ -1344,7 +1344,7 @@ Proof.
 rewrite /cPr.
 have [PF0|PF0] := eqVneq (Pr d F) 0.
   by rewrite setIC (Pr_domin_setI E PF0) div0R.
-apply leR_pdivr_mulr; first by rewrite Pr_gt0.
+apply leR_pdivr_mulr; first by rewrite Pr_gt0P.
 rewrite mul1R /Pr; apply leR_sumRl => //.
   by move=> a _; apply/RleP; rewrite lexx.
 by move=> a; rewrite inE => /andP[].
@@ -1364,16 +1364,18 @@ Qed.
 
 Lemma Pr_cPr_gt0 E F : 0 < Pr d (E :&: F) <-> 0 < `Pr_[E | F].
 Proof.
-rewrite Pr_gt0; split => H; last first.
+rewrite Pr_gt0P; split => H; last first.
   by move/cPr_gt0P : H; apply: contra => /eqP; rewrite /cPr => ->; rewrite div0R.
-rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0 //.
+rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0P //.
 by apply: contra H; rewrite setIC => /eqP F0; apply/eqP/Pr_domin_setI.
 Qed.
 
+(* TODO: rename *)
 Lemma cPr_diff F1 F2 E :
   `Pr_[F1 :\: F2 | E] = `Pr_[F1 | E] - `Pr_[F1 :&: F2 | E].
-Proof. by rewrite /cPr -divRBl setIDAC Pr_diff setIAC. Qed.
+Proof. by rewrite /cPr -divRBl setIDAC Pr_setD setIAC. Qed.
 
+(* TODO: rename *)
 Lemma cPr_union_eq F1 F2 E :
   `Pr_[F1 :|: F2 | E] = `Pr_[F1 | E] + `Pr_[F2 | E] - `Pr_[F1 :&: F2 | E].
 Proof. by rewrite /cPr -divRDl -divRBl setIUl Pr_setU setIACA setIid. Qed.
@@ -1556,7 +1558,7 @@ Definition cPr_eq (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) :=
   locked (`Pr_P[ finset (X @^-1 a) | finset (Y @^-1 b)]).
 Local Notation "`Pr[ X = a | Y = b ]" := (cPr_eq X a Y b).
 
-Lemma cPr_eqE' (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) :
+Lemma cPr_eq_def (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) :
   `Pr[ X = a | Y = b ] = `Pr_P [ finset (X @^-1 a) | finset (Y @^-1 b) ].
 Proof. by rewrite /cPr_eq; unlock. Qed.
 
@@ -1565,19 +1567,19 @@ Notation "`Pr[ X = a | Y = b ]" := (cPr_eq X a Y b) : proba_scope.
 
 #[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_eq`")]
 Notation cpr_eq0 := cPr_eq (only parsing).
-#[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_eqE`")]
-Notation cpr_eqE' := cPr_eqE' (only parsing).
+#[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_eq_def`")]
+Notation cpr_eqE' := cPr_eq_def (only parsing).
 
 Lemma cpr_eq_unit_RV (U : finType) (A : eqType) (P : {fdist U})
     (X : {RV P -> A}) (a : A) :
   `Pr[ X = a | (unit_RV P) = tt ] = `Pr[ X = a ].
-Proof. by rewrite cpr_eqE' cPrET pr_eqE. Qed.
+Proof. by rewrite cPr_eq_def cPrET pr_eqE. Qed.
 
 Lemma cpr_eqE (U : finType) (P : {fdist U}) (TA TB : eqType)
   (X : {RV P -> TA}) (Y : {RV P -> TB}) a b :
   `Pr[ X = a | Y = b ] = `Pr[ [% X, Y] = (a, b) ] / `Pr[Y = b].
 Proof.
-rewrite cpr_eqE' /cPr /dist_of_RV 2!pr_eqE; congr (Pr _ _ / _).
+rewrite cPr_eq_def /cPr /dist_of_RV 2!pr_eqE; congr (Pr _ _ / _).
 by apply/setP => u; rewrite !inE xpair_eqE.
 Qed.
 
@@ -1596,7 +1598,7 @@ Proof. by rewrite /cpr_eq_set; unlock. Qed.
 Lemma cpr_eq_set1 X x (Y : {RV P -> B}) y :
   `Pr[ X \in [set x] | Y \in [set y] ] = `Pr[ X = x | Y = y ].
 Proof.
-by rewrite cpr_eq_setE cpr_eqE'; congr cPr; apply/setP => u; rewrite !inE.
+by rewrite cpr_eq_setE cPr_eq_def; congr cPr; apply/setP => u; rewrite !inE.
 Qed.
 
 End crandom_variable_finType.
@@ -1659,7 +1661,7 @@ Lemma cpr_eq_pairA a b c d :
   `Pr[ [% TX, [% TY, TZ]] = (a, (b, c)) | TW = d ] =
   `Pr[ [% TX, TY, TZ] = (a, b, c) | TW = d].
 Proof.
-rewrite 2!cpr_eqE'; congr (Pr _ _ / _).
+rewrite 2!cPr_eq_def; congr (Pr _ _ / _).
 by apply/setP => u; rewrite !inE /= !xpair_eqE andbA.
 Qed.
 
@@ -1756,13 +1758,13 @@ Lemma cpr_eq_product_rule (U : finType) (P : {fdist U}) (A B C : eqType)
   `Pr[ [% X, Y] = (a, b) | Z = c ] =
   `Pr[ X = a | [% Y, Z] = (b, c) ] * `Pr[ Y = b | Z = c ].
 Proof.
-rewrite cpr_eqE'.
+rewrite cPr_eq_def.
 rewrite (_ : [set x | preim [% X, Y] (pred1 (a, b)) x] =
              finset (X @^-1 a) :&: finset (Y @^-1 b)); last first.
   by apply/setP => u; rewrite !inE xpair_eqE.
-rewrite product_rule_cond cpr_eqE'; congr (cPr _ _ _ * _).
+rewrite product_rule_cond cPr_eq_def; congr (cPr _ _ _ * _).
 - by apply/setP=> u; rewrite !inE xpair_eqE.
-- by rewrite cpr_eqE'.
+- by rewrite cPr_eq_def.
 Qed.
 
 Lemma reasoning_by_cases (U : finType) (P : {fdist U})
@@ -1807,9 +1809,9 @@ Lemma cinde_rv_events : cinde_rv <->
   (forall x y z, cinde_events P (finset (X @^-1 x)) (finset (Y @^-1 y)) (finset (Z @^-1 z))).
 Proof.
 split=> [H /= x y z|/= H x y z].
-- rewrite /cinde_events -2!cpr_eqE' -H cpr_eqE'; congr cPr.
+- rewrite /cinde_events -2!cPr_eq_def -H cPr_eq_def; congr cPr.
   by apply/setP => /= ab; rewrite !inE.
-- rewrite (cpr_eqE' _ x) (cpr_eqE' _ y) -H cpr_eqE'; congr cPr.
+- rewrite (cPr_eq_def _ x) (cPr_eq_def _ y) -H cPr_eq_def; congr cPr.
   by apply/setP => /= ab; rewrite !inE.
 Qed.