proposition: Lemma big_nat_widen : forall 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=> m n1 n2 P F len12; symmetry. rewrite <- big_filter; rewrite filter_predI; rewrite -> big_filter. apply (reducebig_morph _); try reflexivity; try apply H0. rewrite /index_iota; set d1 := n1 - m; set d2 := n2 - m. rewrite -(@subnK d1 d2) /=; last by rewrite leq_sub2r ?leq_addr. have: ~~ has (fun i => i < n1) (iota (m + d1) (d2 - d1)). apply/hasPn=> i; rewrite mem_iota -leqNgt; case/andP=> le_mn1_i _. by apply: leq_trans le_mn1_i; rewrite -leq_sub_add. rewrite -(addnC d1 (d2 - d1)) iota_add filter_cat has_filter /=; case: filter => // _. rewrite cats0; apply/all_filterP; apply/allP=> i. rewrite mem_iota; case/andP=> le_m_i lt_i_md1. apply: (leq_trans lt_i_md1); rewrite subnKC // ltnW //. rewrite -subn_gt0 -(ltn_add2l m) addn0; exact: leq_trans lt_i_md1. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops