proposition: Lemma Bayes_extended j : `Pr_[F j | E] = `Pr_[E | F j] * Pr d (F j) / \sum_(i in I) `Pr_[E | F i] * Pr d (F i).
proof: Proof. have [PE0|PE0] := eqVneq (Pr d E) 0. by rewrite {1 2}/cPr setIC (Pr_domin_setI (F j) PE0) !(div0R,mul0R). rewrite -total_prob_cond /cPr -!mulRA; congr (_ / _). have [Fj0|Fj0] := eqVneq (Pr d (F j)) 0. by rewrite Fj0 !mulR0 (Pr_domin_setI E Fj0). by rewrite setIC mulVR ?mulR1. 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