proposition: Theorem binomial_mono : forall n m p : nat, 2 * m < n -> binomial n (S m - p) <= binomial n (S m).
proof: Proof. intros n m p H; elim p; auto. intros p1 H1; apply Nat.le_trans with (2 := H1). case (Nat.le_gt_cases p1 m); intros H2. rewrite (Nat.sub_succ_l p1 m); simpl in |- *; auto with arith. apply binomial_mono_S. apply Nat.le_lt_trans with (2 := H); auto with arith. apply (fun m n p : nat => Nat.mul_le_mono_l p n m); apply minus_le; auto with arith. repeat rewrite minus_O; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat)