proposition: Lemma big_ltz_cond m n (P : pred int) F : m < n -> let x := \big[op/idx]_(m + 1 <= i < n :> int | P i) F i in \big[op/idx]_(m <= i < n :> int | P i) F i = if P m then op (F m) x else x.
proof: Proof. case: m => m; case: n => n // hmn. - by rewrite /= !big_map big_ltn_cond ?addn1. - case: m hmn => [_ | m]; rewrite NegzE. by rewrite addNr big_map -NegzE /index_iotaz /= big_cons big_map. rewrite addrC subzSS add0r -!NegzE /index_iotaz -(addn1 m.+1). by rewrite /index_iota subn0 iotaD map_cat rev_cat add0n /= big_cons. - case: m hmn => [ | m] //; rewrite !NegzE ltrN2 ltz_nat => hmn. rewrite addrC subzSS add0r -!NegzE /index_iotaz /index_iota subSn //. by rewrite -[(_ - _).+1]addn1 iotaD rev_cat map_cat subnKC // big_cons. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp