proposition: Lemma fdist_self1 : (fdist_self P)`1 = P.
proof: Proof. apply/fdist_ext => a /=; rewrite fdist_fstE (bigD1 a) //= fdist_selfE eqxx /=. by rewrite big1 ?addr0 // => a' /negbTE; rewrite fdist_selfE /= 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