proposition: Theorem power_div_binomial : forall n p r : nat, prime p -> 0 < n -> 2 * n < power p (2 + r) -> power_div (binomial (2 * n) n) p = sum_nm 1 r (fun x => div (2 * n) (power p x) - 2 * div n (power p x)).
proof: Proof. intros n p r H H0 H1. cut (0 < p); [ intros Hp | apply Nat.lt_trans with (2 := lt_prime _ H) ]; auto with arith. rewrite <- sum_nm_minus with (f := fun x => div (2 * n) (power p x)) (g := fun x => 2 * div n (power p x)). apply eq_sym. apply Nat.add_sub_eq_l. rewrite <- sum_nm_times with (f := fun x : nat => div n (power p x)). repeat rewrite <- power_div_fact_prime_div; auto with arith. replace (2 * power_div (factorial n) p) with (power_div (factorial n) p + power_div (factorial n) p); [ idtac | simpl in |- *; ring ]. repeat rewrite <- power_div_mult_prime; auto with arith. apply f_equal2 with (f := power_div); auto with arith. apply sym_equal; replace (2 * n) with (n + n); [ rewrite <- binomial_fact | simpl in |- * ]; ring. replace (2 * n) with (n + n); try apply binomial_lt; auto with arith; ring. apply Nat.le_lt_trans with (2 := H1). simpl in |- *; auto with arith. intros x H2 H3. apply div_mult_le; auto with arith. apply power_lt_O; auto with arith. Qed.
imports: Coq(Wf_nat ArithRing)