proposition: Theorem power_div_binomial1 : forall n p : nat, prime p -> 0 < n -> power p (power_div (binomial (2 * n) n) p) <= 2 * n.
proof: Proof. intros n p H H0. cut (1 < p); [ intros Hp | apply lt_prime ]; auto. cut (0 < p); [ intros Hp1 | apply Nat.lt_trans with (2 := Hp) ]; auto. case (max_such_prop (fun x : nat => power p x <= 2 * n) (fun x => le_dec (power p x) (2 * n)) (2 * n)). exists 0; simpl in |- *; split; auto with arith. case (max_such (fun x : nat => power p x <= 2 * n) (fun x : nat => le_dec (power p x) (2 * n)) (2 * n)); auto. intros H'2 (H1, H2); apply Nat.le_trans with (2 := H1). apply power_le_mono; auto with arith. rewrite power_div_binomial with (r := 0); auto with arith. change (div (2 * n) (power p 1) - 2 * div n (power p 1) <= 0) in |- *. replace (div (2 * n) (power p 1)) with 0; auto with arith. apply sym_equal; apply lt_div_O. apply not_le_lt; apply H2; auto with arith. apply not_le_lt; apply H2; auto with arith. replace (2 + 0) with (2 * 1); auto with arith. intros n1 H'1 (H1, H2); apply Nat.le_trans with (2 := H1). replace (S n1) with (S n1 * 1); auto with arith. rewrite <- sum_nm_c with (p := 1) (c := 1). rewrite power_div_binomial with (r := n1); auto with arith. apply power_le_mono; auto with arith. apply sum_nm_le; auto with arith. intros x H3 H4; apply minus_le. rewrite Nat.add_comm; apply div_mult_lt2; auto with arith. apply power_lt_O; auto with arith. case (Nat.le_gt_cases (2 + n1) (2 * n)); intros Hl. apply not_le_lt; apply H2; auto with arith. apply Nat.lt_trans with (1 := Hl). apply power_id_lt; auto with arith. Qed.
imports: Coq(Wf_nat ArithRing)