# Library prosa.util.bigop

From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop seq div ssrfun.
Consider a sequence of unique elements xs, an element x0, and a predicate P := λ x ⇒ x == x0. Then, any "bigop" over the sequence xs w.r.t. the predicate and a function F is equal to F x0.
Lemma big_pred1_seq :
∀ [R : Type] [idx : R] [op : Monoid.law idx] [X : eqType] [P : pred X] [F : X → R]
(xs : seq X) (i : X),
(i \in xs) →
(uniq xs) →
P =1 pred1 i →
\big[op/idx]_(j <- xs | P j) F j = F i.