Require Import Reals Arith Omega.

(* Goal of the exercise: show that the (p+1)(p+2)...(p+n) is divided by 
  factorial n.
  The solution is that the divisor is C n p, but this is defined as a real
  number, we need to sho that this is an integer. *)

(* The product (p+1)(p+2)...(p+n) will be represented as 
   prod n (fun x => x + p), where prod is the following function. *)
Fixpoint prod (n:nat)(f:nat->nat) : nat :=
  match n with 0 => 1 | S p => f(S p)*prod p f end.

(* This product is also the quotient of two factorials. *)
Lemma prod_fact :  forall n p, prod n (fun x => x + p) * fact p = fact (n+p).
induction n; intros p; simpl; try rewrite <- (IHn p); ring.
Qed.

Hint Resolve INR_fact_neq_0.

(* Now show that the binomial coefficients are integers.
  a simple inductive consequence of Pascal's identity.
  The name of the function "C" can be found by browsing the library, for
  instance using Whelp at http://helm.cs.unibo.it/whelp/ with the 
  search keyword "binomial" *)
Lemma C_nat : forall n p, p <= n -> exists k, C n p = INR k.
Proof.
induction n.
intros p Hp; assert (p=0) by omega; subst p.
exists 1; unfold C; simpl; field.
destruct p as [|p].
unfold C; rewrite <- minus_n_O; exists 1.
simpl (fact 0); simpl (INR 1); field; auto.
intros Hpn; case (le_lt_or_eq _ _ Hpn); clear Hpn; intros Hpn.
rewrite <- pascal; unfold C in *; try omega.
destruct (IHn p) as [k1 Hk1]; try omega.
destruct (IHn (S p)) as [k2 Hk2]; try omega.
exists (k1 + k2).
rewrite plus_INR; rewrite Hk1; rewrite Hk2; auto.
unfold C; rewrite Hpn; rewrite <- minus_n_n; exists 1.
simpl (fact 0); simpl (INR 1); field; auto.
Qed.

Lemma fact_n_div_prod_n : 
  forall n p, exists k, prod n (fun x => x + p) = fact n * k.
Proof.
intros n p; destruct (C_nat (n + p) p) as [k Hk]; try omega; exists k.
apply INR_eq; rewrite mult_INR; rewrite <- Hk; clear Hk k.
replace (INR (prod n (fun x => x + p)%nat)) with
 ( (INR(prod n (fun x:nat => (x + p)%nat)) * INR (fact p)) /(INR (fact p)))%R
 by (field; auto).
rewrite <- mult_INR; rewrite prod_fact; unfold C.
replace (n+p-p) with n by omega.
field; auto.
Qed.