proposition: Theorem prod_nm_le : forall (n m : nat) (f g : nat -> nat), (forall x : nat, n <= x -> x <= n + m -> f x <= g x) -> prod_nm n m f <= prod_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 prod_nm_f; auto with arith. apply Nat.le_trans with (prod_nm n m f * g (n + S m)); auto with arith. repeat rewrite (fun x => Nat.mul_comm x (g (n + S m))); apply (fun m n p : nat => Nat.mul_le_mono_l p n m). 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) Bertrand(Power)