Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids
  Basics.Decidable Spaces.Nat.Core Spaces.Nat.Division Spaces.Nat.Factorial
  Tactics.EvalIn.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Set Universe Minimization ToSet.
Local Unset Elimination Schemes.

Local Open Scope nat_scope.

(** * Binomial coefficients *)

(** ** Definition *)

(** The binomial coefficient [nat_choose n m] is the number of ways to choose [m] elements from a set of [n] elements. We define it recursively using Pascal's identity. We use nested [Fixpoint]s in order to get a function that computes definitionally on the edge cases as well as the inductive case. *)

(** We separate out this helper result to prevent Coq from unfolding things into a larger term. This computes [n] choose [m.+1] given a function [f] that computes [n] choose [m]. *)
Fixpoint nat_choose_step n f :=
  match n with
  | 0 => 0
  | S n' => f n' + nat_choose_step n' f
  end.

Fixpoint nat_choose (n m : nat) {struct m} : nat
  := match m with
    | 0 => 1
    | S m' => nat_choose_step n (fun n => nat_choose n m')
    end.

(** We make sure we never unfold binomial coefficients with [simpl] or [cbn] since the terms do not look good. Instead, we should use lemmas we prove about it to make proofs clearer to read. *)
Arguments nat_choose n m : simpl never.

(** ** Properties *)

(** The three defining properties of [nat_choose] hold definitionally. *)

(** By definition, we have Pascal's identity. *)
Definition nat_choose_succ@{} n m
  : nat_choose n.+1 m.+1 = nat_choose n m + nat_choose n m.+1
  := idpath.

(** There is only one way to choose [0] elements from any number of elements. *)
Definition nat_choose_zero_r@{} n : nat_choose n 0 = 1
  := idpath.

(** There are no ways to choose a non-zero number of elements from [0] elements. *)
Definition nat_choose_zero_l@{} m : nat_choose 0 m.+1 = 0
  := idpath.

(** The binomial coefficient is zero if [m] is greater than [n]. *)
Definition nat_choose_lt@{} n m : n < m -> nat_choose n m = 0.
n, m: nat
n < m -> nat_choose n m = 0
Proof.
n, m: nat
n < m -> nat_choose n m = 0
  revert m; induction n; hnf; intros m H; destruct H.
nat_choose 0 1 = 0
m: nat
H: 1 <= m
nat_choose 0 m.+1 = 0
n: nat
IHn: forall m : nat, n < m -> nat_choose n m = 0
nat_choose n.+1 n.+2 = 0
n: nat
IHn: forall m : nat, n < m -> nat_choose n m = 0
m: nat
H: n.+2 <= m
nat_choose n.+1 m.+1 = 0
  1, 2: reflexivity.
n: nat
IHn: forall m : nat, n < m -> nat_choose n m = 0
nat_choose n.+1 n.+2 = 0
n: nat
IHn: forall m : nat, n < m -> nat_choose n m = 0
m: nat
H: n.+2 <= m
nat_choose n.+1 m.+1 = 0
  1, 2: rewrite_refl nat_choose_succ; exact (ap011 nat_add (IHn _ _) (IHn _ _)).
Defined.

(** There is only one way to choose [n] elements from [n] elements. *)
Definition nat_choose_diag@{} n : nat_choose n n = 1.
n: nat
nat_choose n n = 1
Proof.
n: nat
nat_choose n n = 1
  induction n as [|n IHn]; only 1: reflexivity.
n: nat
IHn: nat_choose n n = 1
nat_choose n.+1 n.+1 = 1
  rewrite_refl nat_choose_succ.
n: nat
IHn: nat_choose n n = 1
nat_choose n n + nat_choose n n.+1 = 1
  rhs_V napply nat_add_zero_r.
n: nat
IHn: nat_choose n n = 1
nat_choose n n + nat_choose n n.+1 = 1 + 0
  napply ap011.
n: nat
IHn: nat_choose n n = 1
nat_choose n n = 1
n: nat
IHn: nat_choose n n = 1
nat_choose n n.+1 = 0
  -
n: nat
IHn: nat_choose n n = 1
nat_choose n n = 1 exact IHn.
  -
n: nat
IHn: nat_choose n n = 1
nat_choose n n.+1 = 0 rapply nat_choose_lt.
Defined.

(** There are [n] ways to choose [1] element from [n] elements. *)
Definition nat_choose_one_r@{} n : nat_choose n 1 = n.
n: nat
nat_choose n 1 = n
Proof.
n: nat
nat_choose n 1 = n
  induction n as [|n IHn]; only 1: reflexivity.
n: nat
IHn: nat_choose n 1 = n
nat_choose n.+1 1 = n.+1
  rewrite_refl nat_choose_succ.
n: nat
IHn: nat_choose n 1 = n
nat_choose n 0 + nat_choose n 1 = n.+1
  exact (ap nat_succ IHn).
Defined.

(** There are [n.+1] ways to choose [n] elements from [n.+1] elements. *)
Definition nat_choose_succ_l_diag@{} n : nat_choose n.+1 n = n.+1.
n: nat
nat_choose n.+1 n = n.+1
Proof.
n: nat
nat_choose n.+1 n = n.+1
  induction n as [|n IHn]; only 1: reflexivity.
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+2 n.+1 = n.+2
  rewrite_refl nat_choose_succ.
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+1 n + nat_choose n.+1 n.+1 = n.+2
  rhs_V napply (nat_add_comm _ 1).
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+1 n + nat_choose n.+1 n.+1 = n.+1 + 1
  napply ap011.
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+1 n = n.+1
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+1 n.+1 = 1
  -
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+1 n = n.+1 exact IHn.
  -
n: nat
IHn: nat_choose n.+1 n = n.+1
nat_choose n.+1 n.+1 = 1 apply nat_choose_diag.
Defined.

(** The binomial coefficients can be written as a quotient of factorials. This is typically used as a definition of the binomial coefficients. *)
Definition nat_choose_factorial@{} n m
  : m <= n -> nat_choose n m = factorial n / (factorial m * factorial (n - m)).
n, m: nat
m <= n ->
nat_choose n m =
factorial n / (factorial m * factorial (n - m))
Proof.
n, m: nat
m <= n ->
nat_choose n m =
factorial n / (factorial m * factorial (n - m))
  revert n m; apply nat_double_ind_leq; intro n.
n: nat
nat_choose n 0 =
factorial n / (factorial 0 * factorial (n - 0))
n: nat
nat_choose n.+1 n.+1 =
factorial n.+1 /
(factorial n.+1 * factorial (n.+1 - n.+1))
n: nat
forall m : nat,
m < n ->
(forall m' : nat,
 m' <= n ->
 nat_choose n m' =
 factorial n / (factorial m' * factorial (n - m'))) ->
nat_choose n.+1 m.+1 =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  (* The case when [m = 0]. *)
  {
n: nat
nat_choose n 0 =
factorial n / (factorial 0 * factorial (n - 0)) rewrite nat_mul_one_l.
n: nat
nat_choose n 0 = factorial n / factorial (n - 0)
    rewrite nat_sub_zero_r.
n: nat
nat_choose n 0 = factorial n / factorial n
    symmetry; rapply nat_div_cancel. }
n: nat
nat_choose n.+1 n.+1 =
factorial n.+1 /
(factorial n.+1 * factorial (n.+1 - n.+1))
n: nat
forall m : nat,
m < n ->
(forall m' : nat,
 m' <= n ->
 nat_choose n m' =
 factorial n / (factorial m' * factorial (n - m'))) ->
nat_choose n.+1 m.+1 =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  (* The case when [m = n]. *)
  {
n: nat
nat_choose n.+1 n.+1 =
factorial n.+1 /
(factorial n.+1 * factorial (n.+1 - n.+1)) rewrite nat_sub_cancel.
n: nat
nat_choose n.+1 n.+1 =
factorial n.+1 / (factorial n.+1 * factorial 0)
    rewrite nat_mul_one_r.
n: nat
nat_choose n.+1 n.+1 = factorial n.+1 / factorial n.+1
    rhs rapply nat_div_cancel.
n: nat
nat_choose n.+1 n.+1 = 1
    napply nat_choose_diag. }
n: nat
forall m : nat,
m < n ->
(forall m' : nat,
 m' <= n ->
 nat_choose n m' =
 factorial n / (factorial m' * factorial (n - m'))) ->
nat_choose n.+1 m.+1 =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  (* The case with [n.+1] and [m.+1] with [m < n] and an induction hypothesis. *)
  intros m H IHn.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
nat_choose n.+1 m.+1 =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite_refl nat_choose_succ.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
nat_choose n m + nat_choose n m.+1 =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite 2 IHn.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
factorial n / (factorial m * factorial (n - m)) +
factorial n / (factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
m.+1 <= n
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
m <= n
  2,3: exact _.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
factorial n / (factorial m * factorial (n - m)) +
factorial n / (factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite <- (nat_div_cancel_mul_l _ _ m.+1).
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(m.+1 * (factorial m * factorial (n - m))) +
factorial n / (factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
0 < m.+1
  2: exact _.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(m.+1 * (factorial m * factorial (n - m))) +
factorial n / (factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite nat_mul_assoc.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(m.+1 * factorial m * factorial (n - m)) +
factorial n / (factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite <- nat_factorial_succ.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
factorial n / (factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite <- (nat_div_cancel_mul_l (factorial n) _ (n - m)).
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
((n - m) * (factorial m.+1 * factorial (n - m.+1))) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
0 < n - m
  2: rapply equiv_lt_lt_sub.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
((n - m) * (factorial m.+1 * factorial (n - m.+1))) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite nat_mul_assoc.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
((n - m) * factorial m.+1 * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite (nat_mul_comm (n - m) (factorial m.+1)).
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
(factorial m.+1 * (n - m) * factorial (n - m.+1)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite <- nat_mul_assoc.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
(factorial m.+1 * ((n - m) * factorial (n - m.+1))) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite nat_sub_succ_r.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
(factorial m.+1 *
 ((n - m) * factorial (nat_pred (n - m)))) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  rewrite <- nat_factorial_pred.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
0 < n - m
  2: rapply equiv_lt_lt_sub.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) +
((n - m) * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  lhs_V napply nat_div_dist.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(factorial m.+1 * factorial (n - m)
| m.+1 * factorial n)
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n + (n - m) * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
  -
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(factorial m.+1 * factorial (n - m)
| m.+1 * factorial n) rewrite nat_factorial_succ.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial m * factorial (n - m)
| m.+1 * factorial n)
    rewrite <- nat_mul_assoc.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * (factorial m * factorial (n - m))
| m.+1 * factorial n)
    exact _.
  -
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(m.+1 * factorial n + (n - m) * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1)) rewrite <- nat_dist_r.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
((m.+1 + (n - m)) * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
    rewrite nat_add_succ_l.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
((m + (n - m)).+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
    rewrite nat_add_sub_r_cancel.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(n.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
m <= n
    2: exact _.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
(n.+1 * factorial n) /
(factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
    rewrite <- nat_factorial_succ.
n, m: nat
H: m < n
IHn: forall m' : nat,
m' <= n ->
nat_choose n m' = factorial n / (factorial m' * factorial (n - m'))
factorial n.+1 / (factorial m.+1 * factorial (n - m)) =
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1))
    reflexivity.
Defined.

(** Another recursive property of the binomial coefficients.  To choose [m+1] elements from a set of size [n+1], one has [n+1] choices for the first element and then can make the remaining [m] choices from the remaining [n] elements.  This overcounts by a factor of [m+1], since there are [m+1] elements that could have been called the "first" element. *)
Definition nat_choose_succ_mul@{} n m
  : nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1.
n, m: nat
nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1
Proof.
n, m: nat
nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1
  destruct (leq_dichotomy m n) as [H | H].
n, m: nat
H: m <= n
nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1
n, m: nat
H: m > n
nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1
  2: {
n, m: nat
H: m > n
nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1 rewrite 2 nat_choose_lt; only 2, 3: exact _.
n, m: nat
H: m > n
0 = (n.+1 * 0) / m.+1
       rewrite nat_mul_zero_r.
n, m: nat
H: m > n
0 = 0 / m.+1
       symmetry; apply nat_div_zero_l. }
n, m: nat
H: m <= n
nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1
  rewrite 2 nat_choose_factorial.
n, m: nat
H: m <= n
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1)) =
(n.+1 *
 (factorial n / (factorial m * factorial (n - m)))) /
m.+1
n, m: nat
H: m <= n
m <= n
n, m: nat
H: m <= n
m.+1 <= n.+1
  2,3: exact _.
n, m: nat
H: m <= n
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1)) =
(n.+1 *
 (factorial n / (factorial m * factorial (n - m)))) /
m.+1
  rewrite nat_div_mul_l.
n, m: nat
H: m <= n
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1)) =
((n.+1 * factorial n) /
 (factorial m * factorial (n - m))) / m.+1
n, m: nat
H: m <= n
(factorial m * factorial (n - m) | factorial n)
  2: exact _.
n, m: nat
H: m <= n
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1)) =
((n.+1 * factorial n) /
 (factorial m * factorial (n - m))) / m.+1
  rewrite nat_div_div_l.
n, m: nat
H: m <= n
factorial n.+1 /
(factorial m.+1 * factorial (n.+1 - m.+1)) =
(n.+1 * factorial n) /
(factorial m * factorial (n - m) * m.+1)
  by rewrite (nat_mul_comm _ m.+1), nat_mul_assoc.
Defined.

(** The binomial coefficients are symmetric about the middle of the range [0 <= n]. *)
Definition nat_choose_sub@{} n m
  : m <= n -> nat_choose n m = nat_choose n (n - m).
n, m: nat
m <= n -> nat_choose n m = nat_choose n (n - m)
Proof.
n, m: nat
m <= n -> nat_choose n m = nat_choose n (n - m)
  intros H.
n, m: nat
H: m <= n
nat_choose n m = nat_choose n (n - m)
  rewrite 2 nat_choose_factorial.
n, m: nat
H: m <= n
factorial n / (factorial m * factorial (n - m)) =
factorial n /
(factorial (n - m) * factorial (n - (n - m)))
n, m: nat
H: m <= n
n - m <= n
n, m: nat
H: m <= n
m <= n
  2,3: exact _.
n, m: nat
H: m <= n
factorial n / (factorial m * factorial (n - m)) =
factorial n /
(factorial (n - m) * factorial (n - (n - m)))
  rewrite nat_sub_sub_cancel_r.
n, m: nat
H: m <= n
factorial n / (factorial m * factorial (n - m)) =
factorial n / (factorial (n - m) * factorial m)
n, m: nat
H: m <= n
m <= n
  2: exact _.
n, m: nat
H: m <= n
factorial n / (factorial m * factorial (n - m)) =
factorial n / (factorial (n - m) * factorial m)
  by rewrite nat_mul_comm.
Defined.