proposition: Lemma big_ltn_cond m n (P : pred nat) F : m < n -> let x := \big[op/idx]_(m.+1 <= i < n | P i) F i in \big[op/idx]_(m <= i < n | P i) F i = if P m then op (F m) x else x.
proof: Proof. by case: n => [//|n] le_m_n; rewrite /index_iota subSn // big_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)