proposition: Lemma big_ltn : forall 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. move=> *; exact: big_ltn_cond. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops