proposition: Lemma Zsum_split_up: forall (n m p : Z) (f : Z -> Z), ( n <= m < p ) -> 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 _ _ H); clear H; intros H. unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. assert (H1: n < p). apply Z.lt_trans with ( 1 := H ); auto with zarith. assert (H2: m < 1 + p). apply Z.lt_trans with ( 1 := H0 ); auto with zarith. assert (H3: n < 1 + m). apply Z.lt_trans with ( 1 := H ); auto with zarith. assert (H4: n < 1 + p). apply Z.lt_trans with ( 1 := H1 ); auto with zarith. replace (Z.abs_nat ((1 + p) - (m + 1))) with (minus (Z.abs_nat ((1 + p) - n)) (Z.abs_nat ((1 + m) - n))). apply iter_progression_app. 1-3: auto with zarith. apply inj_le_rev. (repeat rewrite inj_Zabs_nat); auto with zarith. (repeat rewrite Z.abs_eq); auto with zarith. rewrite next_n_Z. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. apply inj_eq_rev. rewrite inj_minus1. (repeat rewrite inj_Zabs_nat). (repeat rewrite Z.abs_eq); auto with zarith. apply inj_le_rev. (repeat rewrite inj_Zabs_nat). (repeat rewrite Z.abs_eq); auto with zarith. subst m. rewrite Zsum_nn; auto with zarith. unfold Zsum; generalize (Zle_cases n p); generalize (Zle_cases (n + 1) p); case (Zle_bool n p); case (Zle_bool (n + 1) p); auto with zarith. intros H1 H2. replace (Z.abs_nat ((1 + p) - n)) with (S (Z.abs_nat (p - n))). replace (n + 1) with (Z.succ n) by auto with zarith. replace ((1 + p) - Z.succ n) with (p - n); 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