proposition: Theorem binomial_even : forall n : nat, 0 < n -> power 2 (2 * n) <= 2 * n * binomial (2 * n) n.
proof: Proof. intros n Hn. cut (S (2 * n - 2) = 2 * n - 1); [ intros H1 | generalize Hn; case n; simpl in |- *; auto; try (intros H1; inversion H1; fail); (intros n1; repeat rewrite <- plus_n_Sm; simpl in |- *; rewrite Nat.sub_0_r) ]; auto. cut (2 * n - 2 < 2 * n - 1); [ intros H2 | rewrite <- H1; auto with arith ]. cut (S (2 * n - 1) = 2 * n); [ intros H3 | generalize Hn; case n; simpl in |- *; auto; try (intros H3; inversion H3; fail); intros n1; repeat rewrite <- plus_n_Sm; simpl in |- * ]; auto. rewrite binomial2. rewrite sum_nm_split with (r := 0); auto with arith. repeat rewrite <- plus_n_O. rewrite sum_nm_split with (p := 1) (r := 2 * n - 2); auto with arith. replace (1 + (1 + (2 * n - 2))) with (2 * n); [ idtac | generalize H1 H3; simpl in |- *; intros H4; rewrite H4; auto ]. replace (2 * n - 1 - (1 + (2 * n - 2))) with 0; [ idtac | rewrite <- H1, Nat.sub_diag; auto ]. apply Nat.le_trans with (1 + (S (2 * n - 2) * binomial (2 * n) n + 1)). repeat apply Nat.add_le_mono; auto with arith. case n; simpl in |- *; auto. rewrite <- sum_nm_c with (c := binomial (2 * n) n) (p := 1). apply sum_nm_le. intros x Hx H4. assert (Hx2n : x <= 2 * n). apply Nat.le_trans with (1 := H4). pattern (2 * n) at 2; rewrite <- H3; rewrite <- H1; auto with arith. generalize (Nat.lt_succ_pred _ _ Hn); intros H5; rewrite <- H5 at 3. case (Nat.le_gt_cases x n); intros H6. replace x with (S (pred n) - (S (pred n) - x)). apply binomial_mono. rewrite <- H5; auto with arith. rewrite H5; auto with arith. apply Nat.add_sub_eq_l. apply Nat.sub_add; auto. rewrite <- (Nat.sub_add x (2 * n)) at 1; auto with arith. rewrite Nat.add_comm. rewrite binomial_comp with (n := x). rewrite Nat.add_comm, Nat.sub_add; auto with arith. replace (2 * n - x) with (S (pred n) - (x - n)). apply binomial_mono. rewrite <- H5; auto with arith. rewrite H5; auto with arith. replace x with (n + (x - n)) at 2; auto with arith. rewrite Nat.sub_add_distr. replace (2 * n) with (n + n) by ring. rewrite Nat.add_sub; auto. simpl in |- *; rewrite binomial_def3; auto with arith. replace (1 + (S (2 * n - 2) * binomial (2 * n) n + 1)) with (2 + S (2 * n - 2) * binomial (2 * n) n); [ idtac | ring ]. rewrite H1. replace (2 * n * binomial (2 * n) n) with (binomial (2 * n) n + (2 * n - 1) * binomial (2 * n) n). apply Nat.add_le_mono; auto with arith. generalize Hn; elim n; auto with arith. intros n1; case n1; auto with arith. intros n0 H Hn0; replace (2 * S (S n0)) with (S (S (2 * S n0))); auto with arith. 2: simpl in |- *; repeat rewrite <- plus_n_Sm; auto. repeat rewrite binomial_def4; auto with arith. refine (Nat.le_trans _ _ _ _ (Nat.le_add_r _ _)); rewrite Nat.add_comm; auto with arith. pattern (2 * n) at 4 in |- *; rewrite <- H3; auto. Qed.
imports: Coq(Arith ArithRing Wf_nat)