proposition: Lemma jcPr_cplt E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F].
proof: Proof. by move=> PF0; rewrite 2!jcPrE EsetT setCX cPr_cplt ?EsetT // setTE Pr_setTX. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba