proposition: Lemma big_nat_widen m n1 n2 (P : pred nat) F : n1 <= n2 -> \big[op/idx]_(m <= i < n1 | P i) F i = \big[op/idx]_(m <= i < n2 | P i && (i < n1)) F i.
proof: Proof. move=> len12; symmetry; rewrite -big_filter filter_predI big_filter. have [ltn_trans eq_by_mem] := (ltn_trans, irr_sorted_eq ltn_trans ltnn). congr bigop; apply: eq_by_mem; rewrite ?sorted_filter ?iota_ltn_sorted // => i. rewrite mem_filter !mem_index_iota andbCA andbA andb_idr => // /andP[_]. by move/leq_trans->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)