proposition: Theorem Zsum_le: 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 Hl H. unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith. unfold Zsum; 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 x H1; apply H; split. 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; auto with zarith. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression