proposition: Lemma Zsum_S_left: forall (n m : Z) (f : Z -> Z), n < m -> Zsum n m f = f n + Zsum (n + 1) m f.
proof: Proof. intros n m f H; rewrite (Zsum_split_up n n m f); auto with zarith. rewrite Zsum_nn; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression