proposition: Lemma sum_nat_seq_eq1 (I : eqType) r (P : pred I) (F : I -> nat) : (\sum_(i <- r | P i) F i = 1)%N -> exists i, [/\ i \in r, P i, F i = 1 & forall j, j != i -> j \in r -> P j -> F j = 0]%N.
proof: Proof. rewrite big_tnth/= => /eqP/sum_nat_eq1[/= i [Pi Fi FNi]]. exists (tnth (in_tuple r) i); split; rewrite //= ?mem_tnth// => j. move=> /[swap] /(tnthP (in_tuple r))[{} j -> Nij /FNi->//]. by apply: contra_neq Nij => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)