proposition: Lemma big_nat_widen_lr (m1 m2 n1 n2 : nat) (P : pred nat) F : (m2 <= m1)%N -> (n1 <= n2)%N -> \big[op/idx]_(m1 <= i < n1 | P i) F i = \big[op/idx]_(m2 <= i < n2 | P i && (m1 <= i < n1)%N) F i.
proof: Proof. move=> len12 len21; 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; apply/idP/idP; first by case/and3P. move=> himn; rewrite himn; case/andP: himn => h1 h2. by rewrite (leq_trans _ h1) // (leq_trans _ len21). Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp