proposition: Lemma big_prop_seq : forall (I : eqType) (r : seq I) (P : pred I) F, (forall i, P i && (i \in r) -> Pb (F i)) -> Pb (\big[op1/idx]_(i <- r | P i) F i).
proof: Proof. by move=> I r P F; rewrite -> big_cond_seq; exact: big_prop. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops