proposition: Lemma pr_predC E mu: \P_[mu](predC E) = \P_[mu] predT - \P_[mu] E.
proof: Proof. apply/esym/eqP; rewrite subr_eq -pr_or_indep //. by apply/eqP/eq_pr=> x; rewrite !inE orNb. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum