proposition: Theorem sum_nm_le : forall (n m : nat) (f g : nat -> nat), (forall x : nat, n <= x -> x <= n + m -> f x <= g x) -> sum_nm n m f <= sum_nm n m g.
proof: Proof. intros n m f g; generalize n; elim m; clear n m. simpl in |- *; auto with arith. intros m H n H0; repeat rewrite sum_nm_f; auto with arith. apply Nat.add_le_mono; auto with arith. apply H; auto with arith. intros x H1 H2; apply H0; auto with arith. apply Nat.le_trans with (1 := H2); auto with arith. Qed.
imports: Coq(Arith ArithRing)