Upstreamed lemma from `util/bigop.v` to ssreflect
@bbb started a discussion:
> This is a lemma that seems generally useful and missing from ssreflect. Perhaps it could be upstreamed?
Lemma big_pred1_seq :
forall [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.