proposition: Theorem power_div_binomial2 : forall n p : nat, prime p -> 0 < n -> 2 * n < power p 2 -> power_div (binomial (2 * n) n) p <= 1.
proof: Proof. intros n p H H0 H1; generalize (power_div_binomial1 n p H H0). case (power_div (binomial (2 * n) n) p); auto with arith. intros n1; case n1; auto with arith. intros n2 H2; contradict H2; auto with arith. apply Nat.lt_nge; apply Nat.lt_le_trans with (power p 2); auto with arith. apply power_le_mono; auto with arith. apply Nat.lt_trans with 1; auto with arith; apply lt_prime; auto with arith. Qed.
imports: Coq(Wf_nat ArithRing)