proposition: Lemma Zsum_add: forall (n m : Z) (f g : Z -> Z), Zsum n m f + Zsum n m g = Zsum n m (fun (i : Z) => f i + g i).
proof: Proof. intros n m f g; unfold Zsum; case (Zle_bool n m); apply iter_comp; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression