proposition: Lemma Zsum_split_down: forall (n m p : Z) (f : Z -> Z), ( p < m <= n ) -> Zsum n p f = Zsum n m f + Zsum (m - 1) p f.
proof: Proof. intros n m p f [H H0]. case (Zle_lt_or_eq p (m - 1)); auto with zarith; intros H1. pattern m at 1; replace m with ((m - 1) + 1) by auto with zarith. repeat rewrite (Zsum_swap n). rewrite (Zsum_swap (m - 1)). rewrite Zplus_comm. apply Zsum_split_up; auto with zarith. subst p. repeat rewrite (Zsum_swap n). rewrite Zsum_nn. unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. replace (Z.abs_nat ((1 + n) - (m - 1))) with (S (Z.abs_nat (n - (m - 1)))). rewrite Zplus_comm. replace (Z.abs_nat ((1 + n) - m)) with (Z.abs_nat (n - (m - 1))). pattern m at 4; replace m with (Z.succ (m - 1)); auto with zarith. apply f_equal with ( f := Z.abs_nat ); auto with zarith. apply inj_eq_rev. rewrite inj_S. (repeat rewrite inj_Zabs_nat). (repeat rewrite Z.abs_eq); auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression