proposition: Lemma Zsum_times: forall n m x f, x * Zsum n m f = Zsum n m (fun i=> x * f i).
proof: Proof. intros n m x f. unfold Zsum. case (Zle_bool n m); intros; apply iter_comp_const with (k := (fun y : Z => x * y)); auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression