proposition: Lemma cPr_ge0 E F : 0 <= `Pr_[E | F].
proof: 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. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist