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