proposition: Lemma eq_big 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. by move/eq_bigl <-; move/eq_bigr->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)