proposition: Lemma fibration_of_partitionE i x : D i -> F i x -> fibration_of_partition x = Some i.
proof: Proof. move=> Di Fix. rewrite /fibration_of_partition. case: asboolP; last by have : ((\bigcup_(i0 in D) F i0) x) by exists i => //. move=> ?; case: cid2 => j Dj Fjx. congr Some; apply: contrapT; move/eqP => ji. move: disjF => /trivIsetP /(_ j i Dj Di ji). apply/eqP/set0P. by exists x. 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)