proposition: Lemma big_prop : forall I r (P : pred I) F, (forall i, P i -> Pb (F i)) -> Pb (\big[op1/idx]_(i <- r | P i) F i).
proof: Proof. by move=> I r P F PbF; elim: r => //= i *; case Pi: (P i); auto. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops