Theorem pascal_choose: forall k r: nat,
  pascal r k * factorial k = prod_up k (1 + r).
Proof.
  intros.
  induction k.
  *have (pascal r 0 * factorial 0).
   thatis (pascal r 0 * 1).
   rearrange (pascal r 0).
   rewrite (pascal_0 r); have 1.
   thatis (prod_up 0 (1 + r)).
   done.
  *have (pascal r (S k) * factorial (S k)).
   cbn.
Qed.



Fixpoint pascal (row col : nat): nat :=
  match col with
  | S prevcol =>
    match row with
    | S prevrow => pascal prevrow prevcol + pascal prevrow col
    | O => 0 (* First row, not first column... Zero! *)
    end
  | O => 1 (* First column, One! *)
  end.

(* Now we would like to show that this matches the combinatoric 'choose'
   function, so let's define the numerator and denominator of the 'choose'
   function, as two whole-valued functions.

   First the denominator of choose, is the familiar factorial function. *)

Fixpoint factorial (n : nat): nat :=
  match n with
  | S n' => n * factorial n'
  | O => 1
  end.

(* Next the numerator, is the ratio of two factorials, but really it is just
   a small product counding down from some number. Let's implement that
   directly. *)

Fixpoint prod_down (count i0 : nat): nat :=
  match count with
  | O => 1 (* Empty product is 1 *)
  | S count' =>
    match i0 with
    | O => 0 (* Stop counting down at zero. *)
    | S iprev => i0 * prod_down count' iprev
    end
  end.

(* Now before we move on to more complex proofs, let's familiarise ourselves
   with these functions by confirming the relationships we expect them to have.
   First, prod_down from n to 1 should be the same as the factorial of n. *)

Lemma prod_fact : forall n : nat,
  prod_down n n = factorial n.
Proof.
  intro n.
  induction n.
  *want (factorial 0).
   have (prod_down 0 0).
   thatis (factorial 0).
   done.
  *want (factorial (S n)).
   have (prod_down (S n) (S n)).
   thatis (S n * prod_down n n).
   rewrite IHn; have (S n * factorial n).
   thatis (factorial (S n)).
   done.
Qed.

(* That was a nice, simple inductive proof. Let's compare to some of the other
   style that Coq can offer. *)

Lemma prod_fact_opaque : forall n : nat,
  prod_down n n = factorial n.
Proof.
  intro n.
  induction n.
  *trivial. (* Base case is obvious. *)
  *cbn. (* For the inductive case, get Coq to expand everything out. *)
   rewrite IHn. (* Do something with the inductive hypothesis. *)
   trivial. (* You work out the rest. *)
Qed.

(* That proof is far too verbose, though. Let's go back to auto. *)

Lemma prod_fact_auto : forall n : nat,
  prod_down n n = factorial n.
Proof.
  intro n.
  induction n; cbn; auto.
Qed.

(* Perfect. *)

(* Jokes aside, there is another property which is nice to prove, which is that
   prod_down is the ratio of two factorials. We will show this without dipping
   into rationals, by instead multiplying prod_down by factorial to get a
   bigger factorial. *)

Lemma fact_ratio : forall r k : nat,
  prod_down k (k + r) * factorial r = factorial (k + r).
Proof.
  intros r k.
  induction k.
  *want (factorial (0 + r)).
   have (prod_down 0 (0 + r) * factorial r).
   thatis (1 * factorial r).
   thatis (factorial r + 0).
   rearrange (factorial r).
   thatis (factorial (0 + r)).
   done.
  *want (factorial (S k + r)).
   have (prod_down (S k) (S k + r) * factorial r).
   thatis ((S k + r) * prod_down k (k + r) * factorial r).
   weknow Ind: (prod_down k (k + r) * factorial r = factorial (k + r)).
   rearrange ((S k + r) * (prod_down k (k + r) * factorial r)).
   rewrite Ind; have ((S k + r) * (factorial (k + r))).
   thatis (factorial (S k + r)).
   done.
Qed.

(* Another manipulation we can do to these prod_down sequences, is strip one
   term off the bottom. *)

Lemma prod_down_r : forall r k : nat,
  prod_down (1 + k) (1 + k + r) = prod_down k (1 + k + r) * (S r).
Proof.
  intros.
  induction k.
  *have (prod_down (1 + 0) (1 + 0 + r)).
   thatis ((1 + r) * 1).
   rearrange (1 * (1 + r)).
   thatis (prod_down 0 (1 + 0 + r) * S r).
   done.
  *have (prod_down (1 + S k) (1 + S k + r)).
   thatis (prod_down (2 + k) (2 + k + r)).
   thatis ((2 + k + r) * prod_down (1 + k) (1 + k + r)).
   weknow Ind: (prod_down (1 + k) (1 + k + r) = prod_down k (1 + k + r) * S r).
   rewrite Ind.
   have ((2 + k + r) * (prod_down k (1 + k + r) * S r)).
   rearrange (((2 + k + r) * prod_down k (1 + k + r)) * S r).
   thatis (prod_down (S k) (1 + S k + r) * S r).
   done.
Qed.

Lemma prod_down_1: forall r: nat,
  prod_down 1 r = r.
Proof.
  intros.
  destruct r.

Lemma prod_down_r0 : forall r k : nat,
  prod_down (1 + k) (k + r) = prod_down k (k + r) * r.
Proof.
  intros.
  induction k.
  *have (prod_down (1 + 0) (0 + r)).
   cbn.
   thatis ((r + 0) * 1).
   rearrange (1 * r).
   thatis (prod_down 0 (0 + r) * r).
   done.
  *have (prod_down (1 + S k) (1 + S k + r)).
   thatis (prod_down (2 + k) (2 + k + r)).
   thatis ((2 + k + r) * prod_down (1 + k) (1 + k + r)).
   weknow Ind: (prod_down (1 + k) (1 + k + r) = prod_down k (1 + k + r) * S r).
   rewrite Ind.
   have ((2 + k + r) * (prod_down k (1 + k + r) * S r)).
   rearrange (((2 + k + r) * prod_down k (1 + k + r)) * S r).
   thatis (prod_down (S k) (1 + S k + r) * S r).
   done.

(* So we have defined factorials, and ratios between factorials... Now we could
   try and divide one by the other to get a choose function, but we are sort of
   in a bind, in that we need to know the numbers are divisible by one another,
   but to show that constructively, we need to actually compute the whole
   number result anyway. Fortunately our goal was to show that choose matches
   the whole number given by Pascal's triangle, so let's approach it that way
   instead, and show that pascak * factorial = prod_down. *)


Definition weird_fun (col row: nat) :=
  S col * prod_down col row + prod_down (S col) row.

Theorem pascal_choose_weird_fun : forall row col: nat,
  pascal row col * factorial col = prod_down col row ->
  pascal row (S col) * factorial (S col) = prod_down (S col) row ->
  pascal (S row) (S col) * factorial (S col) = weird_fun col row.
Proof.
  intros.
  have (pascal (S row) (S col) * factorial (S col)).
  thatis ((pascal row col + pascal row (S col)) * factorial (S col)).
  rearrange (pascal row col * factorial (S col) + pascal row (S col) * factorial (S col)).
  weknow AboveCase: (pascal row col * factorial col = prod_down col row).
  weknow DiagCase: (pascal row (S col) * factorial (S col) = prod_down (S col) row).
  rewrite DiagCase; have (pascal row col * factorial (S col) + prod_down (S col) row).
  thatis (pascal row col * ((S col) * factorial col) + prod_down (S col) row).
  rearrange (S col * (pascal row col * factorial col) + prod_down (S col) row).
  rewrite AboveCase; have (S col * prod_down col row + prod_down (S col) row).
  thatis (weird_fun col row).
  done.
Qed.

Theorem pascal_choose_weird_step2 : forall r k: nat,
  weird_fun k (1 + k + r) = prod_down (1 + k) (2 + k + r).
Proof.
  intros.
  have (weird_fun k (1 + k + r)).
  thatis (S k * prod_down k (1 + k + r) + prod_down (1 + k) (1 + k + r)).
  rewrite (prod_down_r r k).
  have (S k * prod_down k (1 + k + r) + prod_down k (1 + k + r) * S r).
  rearrange ((2 + k + r) * prod_down k (1 + k + r)).
  thatis (prod_down (1 + k) (2 + k + r)).
  done.
Qed.

Theorem pascal_choose_weird_step3 : forall r k: nat,
  weird_fun k (k + r) = prod_down (1 + k) (1 + k + r).
Proof.
  intros.
  destruct r.
  +have (weird_fun k (k + 0)).
   thatis (S k * prod_down k (k + 0) + prod_down (1 + k) (k + 0)).
   rewrite <- (plus_n_O k).
  intros.
  have (weird_fun k (1 + k + r)).
  thatis (S k * prod_down k (1 + k + r) + prod_down (1 + k) (1 + k + r)).
  rewrite (prod_down_r r k).
  have (S k * prod_down k (1 + k + r) + prod_down k (1 + k + r) * S r).
  rearrange ((2 + k + r) * prod_down k (1 + k + r)).
  thatis (prod_down (1 + k) (2 + k + r)).
  done.
Qed.


  apply eq_sym.
  

  shelve.
  thatis (S (k + r) * prod_down k (k + r)).
  thatis (prod_down (1 + k) (1 + k + r)).
  done.

Theorem pascal_choose_weird_step : forall row col: nat,
  weird_fun col row = prod_down (S col) (S row).
Proof.
  intros.
  have (weird_fun col row).
  thatis (S col * prod_down col row + prod_down (S col) row).
  etransitivity.
  shelve.
  thatis (S row * prod_down col row).
  thatis (prod_down (S col) (S row)).
  done.

Definition normal_fun (col row: nat) :=
  prod_down (S col) (S row).

Definition suspicious_fun (col row: nat) :=
  (S row) * prod_down col row.

Definition f (col row: nat) :=
  (weird_fun col row, normal_fun col row, suspicious_fun col row).


Theorem pascal_choose_case_ss : forall row col: nat,
  pascal row col * factorial col = prod_down col row ->
  pascal row (S col) * factorial (S col) = prod_down (S col) row ->
  pascal (S row) (S col) * factorial (S col) = prod_down (S col) (S row).

Theorem pascal_choose : forall row col : nat,
  pascal row col * factorial col = prod_down col row.
Proof.
  intro row.
  induction row.
  *intro col.
   destruct col.
   +reflexivity.
   +reflexivity.
  *destruct col.
   +reflexivity.
   +have (pascal (S row) (S col) * factorial (S col)).
    thatis ((pascal row col + pascal row (S col)) * factorial (S col)).
    rearrange (pascal row col * factorial (S col) + pascal row (S col) * factorial (S col)).
    weknow Ind: (forall col': nat, pascal row col' * factorial col' = prod_down col' row).
    rewrite (Ind (S col)); have (pascal row col * factorial (S col) + prod_down (S col) row).
    thatis (pascal row col * ((S col) * factorial col) + prod_down (S col) row).
    rearrange (S col * (pascal row col * factorial col) + prod_down (S col) row).
    rewrite (Ind col); have (S col * prod_down col row + prod_down (S col) row).
    destruct row.
   ++destruct col.
   +++reflexivity.
   +++cbn.
      ring.
   ++destruct col.
   +++reflexivity.
   +++ring.
     ring.
  intros row col.
  induction row.
  *destruct col.
   +have (pascal 0 0 * factorial 0).
    thatis 1.
    thatis (prod_down 0 0).
    done.
   +have (pascal 0 (S col) * factorial (S col)).
    thatis 0.
    thatis (prod_down (S col) 0).
    done.
  *destruct col.
   +have (pascal (S row) 0 * factorial 0).
    thatis 1.
    thatis (prod_down 0 (S row)).
    done.
   +cbn.
 want (prod_down col (S row)).
   have (pascal (S row) col * factorial col).
   
 want (prod_down col 0).
   have (pascal 0 col * factorial col)