proposition: Lemma cPr_max E F : `Pr_[E | F] <= 1.
proof: 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. rewrite mul1R /Pr; apply leR_sumRl => //. by move=> a _; apply/RleP; rewrite lexx. by move=> a; rewrite inE => /andP[]. 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