proposition: Lemma sumv_pi_uniq_sum v : uniq (filter P r0) -> v \in V -> \sum_(i <- r0 | P i) sumv_pi_for defV i v = v.
proof: Proof. rewrite /sumv_pi_for defV -!(big_filter r0 P). elim: (filter P r0) v => [|i r IHr] v /= => [_ | /andP[r'i /IHr{}IHr]]. by rewrite !big_nil memv0 => /eqP. rewrite !big_cons eqxx => /addv_pi1_pi2; congr (_ + _ = v). rewrite -[_ v]IHr ?memv_pi2 //; apply: eq_big_seq => j /=. by case: eqP => [<- /idPn | _]; rewrite ?lfunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)