Library binomial

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq bigops fintype.
Require Import div prime choice.

This files contains the definition  of:                                  
  bin m n        ==  binomial coeficients, i.e. m choose n               
                                                                         
In additions to the properties of this function, wilson and pascal are   
two examples of how to manipulate expressions with bigops.               

Import Prenex Implicits.

Lemma fact0 : fact 0 = 1.

Lemma factS : forall n, fact n.+1 = n.+1 * fact n.

Lemma fact_prod n : fact n = \prod_(1 <= i < n.+1) i.

Theorem wilson : forall p, p > 1 -> prime p = (p %| (fact p.-1).+1).


Fixpoint bin_rec (m n : nat) {struct m} :=
  match m, n with
  | m'.+1, n'.+1 => bin_rec m' n + bin_rec m' n'
  | _, 0 => 1
  | 0, _.+1 => 0
  end.

Definition bin := nosimpl bin_rec.

Lemma binE : bin = bin_rec. Qed.

Lemma bin0 : forall n, bin n 0 = 1.

Lemma binS : forall m n, bin m.+1 n.+1 = bin m n.+1 + bin m n.

Lemma bin_small : forall m n, m < n -> bin m n = 0.

Lemma binn : forall n, bin n n = 1.

Lemma bin_gt0 : forall m n, (0 < bin m n) = (n <= m).

Lemma bin_fact : forall m n,
  n <= m -> bin m n * (fact n * fact (m - n)) = fact m.

Lemma bin_sub : forall n m, n <= m -> bin m n = bin m (m - n).

Theorem pascal : forall a b n,
  (a + b) ^ n = \sum_(i < n.+1) (bin n i * (a ^ (n - i) * b ^ i)).