proposition: Lemma fdist_sndE b : fdist_snd b = \sum_(i in A) P (i, b).
proof: Proof. rewrite fdistmapE -(pair_big_snd _ _ (pred1 b)) //=. by apply eq_bigr => a ?; rewrite big_pred1_eq. 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