proposition: Lemma fdist1P (d : R.-fdist A) a : reflect (forall i, i != a -> d i = 0) (d a == 1 :> R).
proof: Proof. apply: (iffP idP) => [/eqP H b ?|H]. - move: (FDist.f1 d); rewrite (bigD1 a) //= H => /esym/eqP. rewrite addrC -subr_eq subrr. by move/eqP/esym/psumr_eq0P => -> // c ca; exact/fdist_ge0. - move: (FDist.f1 d); rewrite (bigD1 a) //= => /esym /eqP. by rewrite -subr_eq => /eqP <-; rewrite big1 // subr0. 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