diff --git a/information_theory/entropy.v b/information_theory/entropy.v
index f55bde35..78c6bfab 100644
--- a/information_theory/entropy.v
+++ b/information_theory/entropy.v
@@ -1333,7 +1333,7 @@ have H2 : cond_entropy (fdistA (fdistAC Q)) = cond_entropy (fdist_prod_of_rV P).
   rewrite -(pair_bigA _ (fun a1 a2 => (fdistA Q)`2 (a1, a2) *
            cond_entropy1 (fdistA Q) (a1, a2))%R) /=.
   apply eq_bigr => v _.
-(* TODO: lemma yyy *)
+(* TODO: lemma *)
   rewrite (@reindex_onto _ _ _ 'rV[A]_n' 'rV[A]_(n' - i)
     (fun w => (castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx v w)))
     (@row_drop A _ i)) /=; last first.
diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v
index e15eba93..c73ddde4 100644
--- a/information_theory/source_coding_fl_direct.v
+++ b/information_theory/source_coding_fl_direct.v
@@ -87,8 +87,8 @@ exists '| up D |.
 rewrite -multE (natRM '| up D | d.+1).
 apply (@leR_trans (IZR `| up D |)); first exact: Rle_up.
 rewrite INR_IZR_INZ inj_Zabs_nat -{1}(mulR1 (IZR _)).
-apply leR_wpmul2l; first exact/IZR_le/Zabs_pos (* TODO: ssrZ? *).
-by rewrite -addn1 natRD /= (_ : 1%:R = 1%R) //; move: (leR0n d) => ?; lra.
+apply:leR_wpmul2l; first exact/IZR_le/normZ_ge0.
+by rewrite (_ : 1 = 1%:R)//; exact/le_INR/leP.
 Qed.
 
 Lemma source_direct_bound d D : { k | D <= (k.+1 * d.+1)%:R }.
diff --git a/probability/convex.v b/probability/convex.v
index 4b826f92..210b50e4 100644
--- a/probability/convex.v
+++ b/probability/convex.v
@@ -365,7 +365,7 @@ Variable A : eqType.
 
 Lemma S1_neq0 a : S1 a != @Zero A. Proof. by []. Qed.
 
-(* TODO: rm? *)
+(* NB: should go away once we do not need coqR anymore *)
 Lemma weight_gt0 a : a != @Zero A -> (0 < weight a)%coqR.
 Proof. by case: a => // p x _ /=. Qed.
 
@@ -745,7 +745,7 @@ have [->|s0] := eqVneq s 0%:pr; first by rewrite p_of_r0 q_of_r0 3!conv0.
 by rewrite convA s_of_pqK// r_of_pqK.
 Qed.
 
-(* TODO: move *)
+(* NB: this is defined here and not in realType_ext.v because it uses the scope %coqR *)
 Lemma onem_probR_ge0 (p: {prob R}) : (0 <= (Prob.p p).~)%coqR.
 Proof. exact/RleP/onem_ge0/prob_le1. Qed.
 Hint Resolve onem_probR_ge0 : core.
@@ -1730,19 +1730,18 @@ have ->: (p + q)%coqR * (/ (p + q))%coqR = 1 by apply mulRV; last by apply Rpos_
 by rewrite !mul1r (addRC p) addrK.
 Qed.
 
-(* TODO: the name conflicts with GRing.scaler0  *)
-Lemma scaler0 : scaler Zero = 0. by []. Qed.
+Lemma scalerZero : scaler Zero = 0. by []. Qed.
 
 Lemma scaler_scalept r x : (0 <= r -> scaler (scalept r x) = r *: scaler x)%coqR.
 Proof.
 case: x => [q y|r0]; last first.
-  by rewrite scalept0// scaler0 !GRing.scaler0.
+  by rewrite scalept0// scalerZero !GRing.scaler0.
 case=> r0.
   by rewrite scalept_gt0 /= scalerA.
 by rewrite -r0 scale0pt scale0r.
 Qed.
 
-Definition big_scaler := big_morph scaler scaler_addpt scaler0.
+Definition big_scaler := big_morph scaler scaler_addpt scalerZero.
 
 Definition avgnr n (g : 'I_n -> E) (e : {fdist 'I_n}) := \sum_(i < n) e i *: g i.
 
diff --git a/probability/proba.v b/probability/proba.v
index 7e81ac2d..70f9b18e 100644
--- a/probability/proba.v
+++ b/probability/proba.v
@@ -1353,7 +1353,7 @@ Qed.
 Lemma cPrET E : `Pr_[E | setT] = Pr d E.
 Proof. by rewrite /cPr setIT Pr_setT divR1. Qed.
 
-Lemma cPrE0 (E : {set A}) : `Pr_[E | set0] = 0.
+Lemma cPrE0 E : `Pr_[E | set0] = 0.
 Proof. by rewrite /cPr setI0 Pr_set0 div0R. Qed.
 
 Lemma cPr_gt0P E F : 0 < `Pr_[E | F] <-> `Pr_[E | F] != 0.
@@ -1378,14 +1378,14 @@ Lemma cPr_setU 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.
 
-Lemma Bayes (E F : {set A}) : `Pr_[E | F] = `Pr_[F | E] * Pr d E / Pr d F.
+Lemma Bayes E F : `Pr_[E | F] = `Pr_[F | E] * Pr d E / Pr d F.
 Proof.
 have [PE0|PE0] := eqVneq (Pr d E) 0.
   by rewrite /cPr [in RHS]setIC !(Pr_domin_setI F PE0) !(div0R,mul0R).
 by rewrite /cPr -mulRA mulVR // mulR1 setIC.
 Qed.
 
-Lemma product_rule (E F : {set A}) : Pr d (E :&: F) = `Pr_[E | F] * Pr d F.
+Lemma product_rule E F : Pr d (E :&: F) = `Pr_[E | F] * Pr d F.
 Proof.
 rewrite /cPr; have [PF0|PF0] := eqVneq (Pr d F) 0.
   by rewrite setIC (Pr_domin_setI E PF0) div0R mul0R.
@@ -1404,7 +1404,7 @@ rewrite -{1}(@setIT _ E) -(setUCr F) setIC setIUl disjoint_Pr_setU //.
 by rewrite -setI_eq0 setIACA setICr set0I.
 Qed.
 
-Lemma inde_events_cPr (E F : {set A}) : Pr d F != 0 -> inde_events d E F ->
+Lemma inde_events_cPr E F : Pr d F != 0 -> inde_events d E F ->
   `Pr_[E | F] = Pr d E.
 Proof. by move=> F0 EF; rewrite /cPr EF /Rdiv -mulRA mulRV ?mulR1. Qed.