proposition: Theorem Zsum_lt: forall n m f g, (forall x, n <= x -> x <= m -> f x <= g x) -> (exists x, n <= x /\ x <= m /\ f x < g x) -> Zsum n m f < Zsum n m g.
proof: Proof. intros n m f g H (d, (Hd1, (Hd2, Hd3))); unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith. cut (In d (progression Z.succ n (Z.abs_nat (1 + m - n)))). cut (forall x, In x (progression Z.succ n (Z.abs_nat (1 + m - n)))-> f x <= g x). elim (progression Z.succ n (Z.abs_nat (1 + m - n))); simpl; auto with zarith. intros a l Rec H0 [H1 | H1]; subst; auto. apply Z.le_lt_trans with (f d + iter 0 g Zplus l); auto with zarith. apply Zplus_le_compat_l. apply iter_le; auto. apply Z.lt_le_trans with (f a + iter 0 g Zplus l); auto with zarith. intros x H1; apply H. apply Zprogression_le_init with ( 1 := H1 ); auto. cut (x < m + 1); auto with zarith. replace (m + 1) with (n + Z_of_nat (Z.abs_nat ((1 + m) - n))). apply Zprogression_le_end with ( 1 := H1 ); auto with arith. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. apply in_Zprogression. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression