proposition: Lemma big_ltn m n F : m < n -> \big[op/idx]_(m <= i < n) F i = op (F m) (\big[op/idx]_(m.+1 <= i < n) F i).
proof: Proof. by move=> lt_mn; apply: big_ltn_cond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)