proposition: Theorem Zsum_com: forall (i j k l : Z) (f : Z -> Z -> Z), Zsum i j (fun x => Zsum k l (fun y => f x y)) = Zsum k l (fun y => Zsum i j (fun x => f x y)).
proof: Proof. intros; unfold Zsum; case (Zle_bool i j); case (Zle_bool k l); apply iter_com; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression