proposition: Lemma fdist1E1 (d' : fdist R A) a : (d' a == 1 :> R) = (d' == fdist1 a :> R.-fdist A).
proof: Proof. apply/idP/idP => [Pa1|/eqP ->]; last by rewrite fdist1E eqxx. apply/eqP/fdist_ext => a0; rewrite fdist1E. have [->|Ha] := eqVneq a0 a; first exact/eqP. by move/fdist1P : Pa1 => ->. 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