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