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