proposition: Theorem Zsum_minus: forall n m f g, Zsum n m f - Zsum n m g = Zsum n m (fun x => f x - g x).
proof: Proof. intros n m f g; apply trans_equal with (Zsum n m f + (-1) * Zsum n m g); auto with zarith. rewrite Zsum_times; rewrite Zsum_add; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression