proposition: Lemma big_ltz m n F : m < n -> \big[op/idx]_(m <= i < n :> int) F i = op (F m) (\big[op/idx]_(m + 1 <= i < n :> int) F i).
proof: Proof. move=> lt_mn; exact: big_ltz_cond. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp