proposition: Lemma big_addz2l n a (P : pred int) F : \big[op/idx]_(a <= i < a + n :> int | P i) F i = \big[op/idx]_(0 <= i < n :> int | P (i + a)) F (i + a).
proof: Proof. by rewrite -{1}(add0r a) big_addz -addrAC subrr add0r. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp