proposition: Lemma eq_big : forall r (P1 P2 : pred I) F1 F2, P1 =1 P2 -> (forall i, P1 i -> F1 i === F2 i) -> \big[op/idx]_(i <- r | P1 i) F1 i === \big[op/idx]_(i <- r | P2 i) F2 i.
proof: Proof. move=> r P1 P2 F1 F2; move/eq_bigl=> Heq; rewrite <- Heq=>{Heq}. move/eq_bigr=> Heq; rewrite -> Heq=>{Heq}; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops