proposition: Lemma fdist_uniform_supp_distrr g : \sum_(t in C) ((`U HC) t * g t) = (#|C|%:R^-1 * \sum_(t in C) g t) :> R.
proof: Proof. rewrite /= big_distrr /=; apply eq_bigr => /= i Hi. by rewrite fdist_uniform_supp_in. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext