proposition: Theorem power_div_binomial3 : forall n p : nat, prime p -> 2 < n -> 2 * n < 3 * p -> p <= n -> power_div (binomial (2 * n) n) p = 0.
proof: Proof. intros n p Hp Hn Hp1 Hp2. cut (1 < p); [ intros Hp3 | apply lt_prime ]; auto. cut (0 < p); [ intros Hp4 | apply Nat.lt_trans with (2 := Hp3) ]; auto. 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 |- *. repeat rewrite power_SO. replace (div (2 * n) p) with 2. replace (div n p) with 1; auto with arith. apply div_unique; auto with arith. rewrite Nat.mul_1_r; auto. apply Nat.add_lt_mono_l with (p := p). apply Nat.le_lt_trans with (n + n); auto with arith. replace (n + n) with (2 * n); auto with arith. replace (p + p * (1 + 1)) with (3 * p); auto with arith. rewrite (Nat.mul_comm p); simpl in |- *; ring. simpl in |- *; ring. apply div_unique; auto with arith. rewrite (Nat.mul_comm p); auto with arith. replace (p * (1 + 2)) with (3 * p); auto with arith. apply Nat.lt_trans with (2 := Hn); auto. apply Nat.lt_le_trans with (1 := Hp1). replace (power p (2 + 0)) with (p * p). case (prime_2_or_more p); auto with arith. intros H1; contradict Hp1; auto with arith. apply Nat.le_ngt. rewrite (fun x => Nat.mul_comm x p); rewrite H1; auto with arith. repeat rewrite (fun x => Nat.mul_comm x p); auto with arith. simpl in |- *; rewrite Nat.mul_1_r; auto. Qed.
imports: Coq(Wf_nat ArithRing)