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