proposition: Lemma eq_big_nat m n F1 F2 : (forall i, m <= i < n -> F1 i = F2 i) -> \big[op/idx]_(m <= i < n) F1 i = \big[op/idx]_(m <= i < n) F2 i.
proof: Proof. by move=> eqF; apply: congr_big_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)