proposition: Theorem binomial_odd : forall n : nat, binomial (2 * n + 1) (n + 1) <= power 2 (2 * n).
proof: Proof. intros n. case (le_lt_eq_dec 0 n); auto with arith; intros H1. apply (Nat.mul_le_mono_pos_l _ _ 2); auto with arith. pattern 2 at 3 in |- *; rewrite <- (power_SO 2). rewrite power_mult. replace (1 + 2 * n) with (2 * n + 1) by apply Nat.add_comm. replace (2 * binomial (2 * n + 1) (n + 1)) with (binomial (2 * n + 1) n + binomial (2 * n + 1) (n + 1)). rewrite binomial2. rewrite sum_nm_split with (r := pred n). replace (1 + (0 + pred n)) with n; auto with arith. replace (2 * n + 1 - (1 + pred n)) with (n + 1); auto with arith. apply Nat.le_trans with (sum_nm n (n + 1) (fun x : nat => binomial (2 * n + 1) x)); auto with arith. rewrite sum_nm_split with (r := 1). apply Nat.le_trans with (sum_nm n 1 (fun x : nat => binomial (2 * n + 1) x)); auto with arith. replace (n + 1) with (S n); simpl in |- *; auto; rewrite Nat.add_comm; auto. replace 1 with (0 + 1); auto with arith. simpl in |- *; rewrite (Nat.lt_succ_pred 0); auto with arith. rewrite <- Nat.add_assoc, (Nat.add_comm _ (_ + 1)), Nat.add_sub; ring. simpl in |- *; rewrite (Nat.lt_succ_pred 0); auto with arith. apply Nat.le_lt_trans with n; auto with arith. pattern n at 1 in |- *; replace n with (n + 0); auto with arith. replace (2 * n + 1) with (n + (n + 1)); auto with arith. simpl in |- *; ring. replace (2 * n + 1) with (n + (n + 1)); auto with arith. rewrite (binomial_comp n). simpl in |- *; ring. simpl in |- *; ring. rewrite <- H1; simpl in |- *; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat)