proposition: Lemma fdistmapE (b : B) : fdistmap b = \sum_(a in A | a \in g @^-1 b) p a.
proof: Proof. rewrite /fdistmap fdistbindE [in RHS]big_mkcond /=; apply eq_bigr => a _. case: ifPn => [|]; first by rewrite inE => /eqP->; rewrite fdist1xx mulr1. by rewrite !inE => gab; rewrite fdist10 ?mulr0// eq_sym. 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