proposition: Lemma fbig_pred1_inj (A : choiceType) (C : eqType) h (k : A -> C) (d : {fset _}) a : a \in d -> injective k -> \big[op/idx]_(a0 <- d | k a0 == k a) h a0 = h a.
proof: Proof. move=> ad inj_k. rewrite big_fset_condE -(big_seq_fset1 op); apply eq_fbig => // a0. rewrite !inE /=; apply/idP/idP => [|/eqP ->]; last by rewrite eqxx andbT. by case/andP => _ /eqP/inj_k ->. 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