proposition: Theorem Zsum_c: forall (c p q : Z), p <= q -> Zsum p q (fun x => c) = ((1 + q) - p) * c.
proof: Proof. intros c p q Hq; unfold Zsum. rewrite Zle_imp_le_bool; auto with zarith. pattern ((1 + q) - p) at 2. rewrite <- Z.abs_eq; auto with zarith. rewrite <- inj_Zabs_nat; auto with zarith. cut (exists r , r = Z.abs_nat ((1 + q) - p) ); [intros [r H1]; rewrite <- H1 | exists (Z.abs_nat ((1 + q) - p))]; auto. generalize p; elim r; auto with zarith. intros n H p0; replace (Z_of_nat (S n)) with (Z_of_nat n + 1). simpl; rewrite H; ring. rewrite inj_S; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression