proposition: Lemma natr_sum_eq1 (I : finType) (P : pred I) (F : I -> R) : (forall i, P i -> F i \is a nat_num) -> \sum_(i | P i) F i = 1 -> {i : I | [/\ P i, F i = 1 & forall j, j != i -> P j -> F j = 0]}.
proof: Proof. move=> natF /eqP; rewrite -sum_truncK// -[1]/1%:R eqr_nat => /sum_nat_eq1 exi. have [i /and3P[Pi /eqP f1 /forallP a]] : {i : I | [&& P i, trunc (F i) == 1 & [forall j : I, ((j != i) ==> P j ==> (trunc (F j) == 0))]]}. apply/sigW; have [i [Pi /eqP f1 a]] := exi; exists i; apply/and3P; split=> //. by apply/forallP => j; apply/implyP => ji; apply/implyP => Pj; apply/eqP/a. exists i; split=> [//||j ji Pj]; rewrite -[LHS]truncK ?natF ?f1//; apply/eqP. by rewrite -[0]/0%:R eqr_nat; apply: implyP Pj; apply: implyP ji; apply: a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)