proposition: Lemma inv_Zsum: forall (P : Z -> Prop) (n m : Z) (f : Z -> Z), n <= m -> P 0 -> (forall (a b : Z), P a -> P b -> P (a + b)) -> (forall (x : Z), ( n <= x <= m ) -> P (f x)) -> P (Zsum n m f).
proof: Proof. intros P n m f HH H H0 H1. unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith; apply iter_inv; auto. intros x H3; apply H1; auto; split. apply Zprogression_le_init with ( 1 := H3 ). cut (x < 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