proposition: Theorem binomial_mono_S : forall n m : nat, 2 * m < n -> binomial n m <= binomial n (S m).
proof: Proof. intros n; elim n; simpl in |- *; auto with arith. intros m; case m; simpl in |- *; auto with arith. clear n; intros n Rec m; case m; clear m. case n; simpl in |- *; auto with arith. intros m; rewrite <- plus_n_O; rewrite <- plus_n_Sm; intros Hm. case (le_lt_eq_dec (S (S (m + m))) n); auto with arith; intros H1. rewrite (Nat.add_comm (binomial n (S m))). apply Nat.add_le_mono; auto. apply Nat.le_trans with (binomial n (S m)); auto with arith. apply Rec; rewrite <- plus_n_O; auto with arith. apply Nat.lt_trans with (S m + m); auto with arith. apply Rec; rewrite <- plus_n_O; rewrite <- plus_n_Sm; auto with arith. replace n with (S (S m) + m). rewrite binomial_comp with (n := S (S m)). rewrite (Nat.add_comm (binomial (S (S m) + m) (S m))); auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat)