proposition: Lemma Zsum_ext: forall (n m : Z) (f g : Z -> Z), n <= m -> (forall (x : Z), ( n <= x <= m ) -> f x = g x) -> Zsum n m f = Zsum n m g.
proof: Proof. intros n m f g HH H. unfold Zsum; auto. unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. apply iter_ext; auto with zarith. intros a H1; apply H; auto; split. apply Zprogression_le_init with ( 1 := H1 ). cut (a < Z.succ m); auto with zarith. replace (Z.succ m) with (n + Z_of_nat (Z.abs_nat ((1 + m) - n))). apply Zprogression_le_end; auto with zarith. rewrite inj_Zabs_nat. (repeat rewrite Z.abs_eq); auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression