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.