proposition: Theorem Zsum_Zsum_f: forall (i j k l : Z) (f : Z -> Z -> Z), i <= j -> k < l -> Zsum i j (fun x => Zsum k (l + 1) (fun y => f x y)) = Zsum i j (fun x => Zsum k l (fun y => f x y) + f x (l + 1)).
proof: Proof. intros; apply Zsum_ext; intros; auto with zarith. rewrite Zsum_S_right; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression