proposition: Lemma sum_nat_eq1 (I : finType) (P : pred I) (F : I -> nat) : reflect (exists i : I, [/\ P i, F i = 1 & forall j, j != i -> P j -> F j = 0]%N) (\sum_(i | P i) F i == 1)%N.
proof: Proof. apply/(iffP idP) => [sumF_eq1 | [i [Pi Fi1 zFj]]]; last first. rewrite (bigD1 i)//= Fi1 addn_eq1//= orbF sum_nat_eq0. by apply/forall_inP => j /andP[Pj ji]; apply/eqP/zFj. have /forall_inPn [i Pi FiN0]: ~~ [forall i in P, F i == 0]. by apply: contraTN sumF_eq1 => /'forall_in_eqP F0; rewrite big1. move: sumF_eq1; rewrite (bigD1 i)//= addn_eq1 (negPf FiN0)/= orbF. move=> /andP[/eqP Fi1]; rewrite sum_nat_eq0 => /'forall_in_eqP FNi0. by exists i; split; rewrite // => j /[swap] Nij /(conj Nij)/andP/FNi0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)