proposition: Lemma eq_bigr : forall r (P : pred I) F1 F2, (forall i, P i -> F1 i === F2 i) -> \big[op/idx]_(i <- r | P i) F1 i === \big[op/idx]_(i <- r | P i) F2 i.
proof: Proof. move=> r P F1 F2 eqF12. elim: r => //=;try reflexivity; move=> x r H1. case Px: (P x); last by assumption. apply H0; [apply eqF12; assumption|rewrite -> H1; reflexivity]. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops