proposition: Lemma Zsum_pred: forall (n m : Z) (f : Z -> Z), Zsum n m f = Zsum (n + 1) (m + 1) (fun (i : Z) => f (Z.pred i)).
proof: Proof. intros n m f. unfold Zsum. generalize (Zle_cases n m); generalize (Zle_cases (n + 1) (m + 1)); case (Zle_bool n m); case (Zle_bool (n + 1) (m + 1)); auto with zarith. replace ((1 + (m + 1)) - (n + 1)) with ((1 + m) - n); auto with zarith. intros H1 H2; cut (exists c , c = Z.abs_nat ((1 + m) - n) ). intros [c H3]; rewrite <- H3. generalize n; elim c; auto with zarith; clear H1 H2 H3 c n. intros c H n; simpl; eq_tac; auto with zarith. eq_tac; unfold Z.pred; auto with zarith. replace (Z.succ (n + 1)) with (Z.succ n + 1); auto with zarith. exists (Z.abs_nat ((1 + m) - n)); auto. replace ((1 + (n + 1)) - (m + 1)) with ((1 + n) - m); auto with zarith. intros H1 H2; cut (exists c , c = Z.abs_nat ((1 + n) - m) ). intros [c H3]; rewrite <- H3. generalize n; elim c; auto with zarith; clear H1 H2 H3 c n. intros c H n; simpl; (eq_tac; auto with zarith). eq_tac; unfold Z.pred; auto with zarith. replace (Z.pred (n + 1)) with (Z.pred n + 1); auto with zarith. unfold Z.pred; auto with zarith. exists (Z.abs_nat ((1 + n) - m)); auto. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression