probability_fin can be avoided

theories/measure.v

@@ -3534,12 +3534,6 @@ move=> mA; rewrite -(@probability_setT _ _ _ P).
 by apply: le_measure => //; rewrite ?in_setE.
 Qed.
 
-Lemma probability_fin (A : set T) : measurable A -> P A \is a fin_num.
-Proof.
-move=> Ameas; rewrite ge0_fin_numE//.
-by rewrite (@le_lt_trans _ _ 1)// ?measure_ge0 ?probability_le1// ?ltey.
-Qed.
-
 Lemma probability_setC (A : set T) : measurable A -> P (~` A) = 1 - P A.
 Proof.
 move=> mA.

theories/prob_lang.v

@@ -314,7 +314,7 @@ rewrite (_ : (fun x => _) = (fun x => x *
   apply/funext => x; case: ifPn => ix; first by rewrite indicE/= mem_set ?mule1.
   by rewrite indicE/= memNset ?mule0// /= in_itv/=; exact/negP.
 apply: emeasurable_funM => //=; apply/measurable_EFinP.
-by rewrite (_ : \1__ = mindic R (emeasurable_itv `[(i%:R)%:E, (i.+1%:R)%:E[)).
+by rewrite (_ : \1__ = mindic R (emeasurable_itv `[i%:R%:E, i.+1%:R%:E[)).
 Qed.
 
 Definition mk i t := [the measure _ _ of k mf i t].
@@ -1395,14 +1395,14 @@ Let q : R := p * (1 - p).
 Let r : R := p ^+ 2 + (1 - p) ^+ 2.
 
 Let Dtrue : D [set true] = p%:E.
-Proof. by rewrite fineK//= probability_fin. Qed.
+Proof. by rewrite fineK//= fin_num_measure. Qed.
 
 Let Dfalse : D [set false] = 1 - (p%:E).
 Proof.
 rewrite -Dtrue; have <- : D [set: bool] = 1 := probability_setT.
 rewrite setT_bool measureU//=; last first.
   by rewrite disjoints_subset => -[]//.
-by rewrite addeAC subee ?probability_fin ?add0e.
+by rewrite addeAC subee ?fin_num_measure ?add0e.
 Qed.
 
 Let p_ge0 : (0 <= p)%R.
@@ -1510,7 +1510,7 @@ by rewrite sumgE ltey.
 Unshelve. all: end_near. Qed.
 
 Lemma von_neumann_trick_prob_kernelT gamma :
-   von_neumann_trick gamma [set: bool] = 1.
+  von_neumann_trick gamma [set: bool] = 1.
 Proof.
 rewrite setT_bool measureU//=; last first.
   by rewrite disjoints_subset => -[].