proposition: Lemma big_add1 : forall m n (P : pred nat) F, \big[op/idx]_(m.+1 <= i < n | P i) F i === \big[op/idx]_(m <= i < n.-1 | P (i.+1)) F (i.+1).
proof: Proof. move=> m n P F; rewrite -addn1; rewrite -> big_addn, subn1. by apply: eq_big => ? *; rewrite addn1;try reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops