Coq proof that factorial N / (factorial k * factorial (N-k)) is integer

Question

I could not find the proof that N choose k is intergral in the Coq standard library. What would be a short self-contained proof of this lemma?

Lemma fact_divides N k: k <= N -> Nat.divide (fact k * fact (N - k)) (fact N).

I saw that in ssreflect.binomial.v they sidestepped the entire problem by defining choose recursively, choose(N,k) = choose(N-1,k) + choose(N-1,k-1), and then show that choose(N,k) * k! * (N-k)! = N!.

However, it would be nice to have a direct proof of the above, too, without resorting to pascal's triangle. Many of the "informal" proofs that come up when I search for it here on Stack.* implicitly use algebra steps for rational numbers, and they don't bother showing that it works for strictly nat division.

EDIT: Thanks to @Bubbler's answer below (based on this math), the proof is just

intros. destruct (fact_div_fact_fact k (N - k)) as [d Hd]. exists d. rewrite <- Hd. apply f_equal. omega.

Answer 1

Instead of unwieldy minus, I'd state it as follows:

Theorem fact_div_fact_fact : forall x y, exists e, fact (x + y) = e * (fact x * fact y).

I believe you can derive your own lemma from this, combined with facts about <= and - in the Coq standard library.

And here is the self-contained, not-so-short proof using the pure algebraic approach. You can try running it here online.

From Coq Require Import Arith.

(* Let's prove that (n+m)! is divisible by n! * m!. *)

(* fact2 x y = (x+1) * (x+2) * .. * (x+y) *)

Fixpoint fact2 x y := match y with
  | O => 1
  | S y' => (x + y) * fact2 x y'
end.

Lemma fact2_0 : forall x, fact2 0 x = fact x.
Proof.
  induction x.
  - auto.
  - simpl. rewrite IHx. auto. Qed.

Lemma fact_fact2 : forall x y, fact x * fact2 x y = fact (x + y).
Proof.
  induction x.
  - intros. simpl. rewrite fact2_0. ring.
  - induction y.
    + simpl. replace (x + 0) with x by ring. ring.
    + simpl. replace (x + S y) with (S x + y) by ring. rewrite <- IHy. simpl. ring. Qed.

Lemma fact2_left : forall x y, fact2 x (S y) = S x * fact2 (S x) y.
Proof. intros x y. generalize dependent x. induction y.
  - intros. simpl. ring.
  - intros. unfold fact2. fold (fact2 x (S y)). fold (fact2 (S x) y).
    rewrite IHy. ring. Qed.

Lemma fact_div_fact2 : forall x y, exists e, fact2 x y = e * fact y.
Proof. intros x y. generalize dependent x. induction y.
  - intros. simpl. exists 1. auto.
  - induction x.
    + unfold fact2. fold (fact2 0 y). unfold fact. fold (fact y). destruct (IHy 0). rewrite H.
      exists x. ring.
    + unfold fact2. fold (fact2 (S x) y).
      destruct (IHy (S x)). destruct IHx. exists (x0 + x1).
      replace ((S x + S y) * fact2 (S x) y) with (S x * fact2 (S x) y + S y * fact2 (S x) y) by ring.
      rewrite <- fact2_left. rewrite H0. rewrite H.
      replace (S y * (x0 * fact y)) with (x0 * (S y * fact y)) by ring.
      unfold fact. fold (fact y). ring. Qed.

Theorem fact_div_fact_fact : forall x y, exists e, fact (x + y) = e * (fact x * fact y).
Proof. intros x y. destruct (fact_div_fact2 x y). exists x0.
  rewrite <- fact_fact2. rewrite H. ring. Qed.