proposition: Lemma big_nat_widenl (m1 m2 n : nat) (P : pred nat) F : m2 <= m1 -> \big[op/idx]_(m1 <= i < n | P i) F i = \big[op/idx]_(m2 <= i < n | P i && (m1 <= i)) F i.
proof: Proof. move=> le_m21; have [le_nm1|lt_m1n] := leqP n m1. rewrite big_geq// big_nat_cond big1//. by move=> i /and3P[/andP[_ /leq_trans/(_ le_nm1)/ltn_geF->]]. rewrite big_mkcond big_mkcondl (big_cat_nat _ _ le_m21) 1?ltnW//. rewrite [X in op X]big_nat_cond [X in op X]big_pred0; last first. by move=> k; case: ltnP; rewrite andbF. by rewrite Monoid.mul1m; apply: congr_big_nat => // k /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)