proposition: Lemma in_fibration_of_partition (x : T) : if fibration_of_partition x is Some i then x \in F i else true.
proof: Proof. rewrite /fibration_of_partition /=. case/asboolP: ((\bigcup_(i in D) F i) x) => //=. case/cid2 => *. by rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex mathcomp(measure probability)