proposition: Lemma Zsum_nn: forall n f, Zsum n n f = f n.
proof: Proof. intros n f; unfold Zsum; rewrite Zle_bool_refl. replace ((1 + n) - n) with 1; auto with zarith. simpl; ring. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression