proposition: Lemma fdist_supp_neq0 (d : fdist R A) : fdist_supp d != set0.
proof: Proof. apply/eqP => H; move: (FDist.f1 d). rewrite -[LHS]mulr1 big_distrl sum_fdist_supp H big1 //=. by move=> /esym/eqP; rewrite oner_eq0. by move=> i; rewrite inE. 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