proposition: Lemma big_addz m n a (P : pred int) F : \big[op/idx]_(m + a <= i < n :> int | P i) F i = \big[op/idx]_(m <= i < n - a :> int | P (i + a)) F (i + a).
proof: Proof. suff -> : index_iotaz (m + a) n = map (fun i => i + a) (index_iotaz m (n - a)). by rewrite big_map. apply: (@eq_from_nth _ 0). by rewrite size_map !size_index_iotaz lerBDl addrC -addrA opprD. move=> i; rewrite size_index_iotaz; case: ifP => // hman hi. rewrite nth_index_iotaz // (nth_map 0); last first. rewrite size_index_iotaz lerBDr hman. by move: hi; rewrite opprD -addrCA addrC. rewrite nth_index_iotaz 1?addrAC // ?lerBDr //. by move: hi; rewrite opprD addrA. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp