proposition: Lemma denE : den = fdistmap K e i.
proof: Proof. rewrite /den !fdistE [RHS]big_mkcond /=. under eq_bigl do rewrite inE. apply/eq_bigr => a _. rewrite !fdistE /= (big_pred1 (a,i)) ?fdistE /=; last by case=> x y; rewrite /swap /= !xpair_eqE andbC. rewrite eq_sym 2!inE. by case: eqP => // _; rewrite (mulr0,mulr1). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex