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