Require Import Arith.
Require Import Omega.

Fixpoint comb (k n:nat) {struct n} : nat :=
   match n with O => match k with O => (1%nat) | (S l) => O end
          | (S m) => match k with O => (1%nat)
                            | (S l) => ((comb l m) + (comb k m))%nat
                     end
   end.

Lemma comb_0_n : forall n, comb 0 n = 1%nat.

Lemma comb_not_le : forall n k, (S n <= k)%nat -> comb k n = 0%nat.

Lemma comb_Sn_n : forall n, comb (S n) n = 0%nat.

Lemma comb_n_n : forall n, comb n n = 1%nat.

Lemma comb_1_Sn : forall n, comb 1 (S n) = S n.

Lemma comb_inv : forall n k, (k<=n)%nat -> comb k n = comb (n-k) n.

Lemma comb_n_Sn : forall n, comb n (S n) = (S n).

Notation H := (fun n k => comb (S k) (S n) * (S k) = comb k (S n) * (S n - k)).
Notation V := (fun n k => comb k (S n) * (S n - k) = comb k n * (S n)).

Lemma comb_relations : forall n k, H n k /\ V n k.

Lemma comb_incr_n : forall n k, comb k (S n) * (S n - k) = comb k n * (S n).

Lemma comb_incr_k : forall n k, comb (S k) (S n) * (S k) = comb k (S n) * (S n - k).

Lemma comb_fact : forall n k, k<=n -> comb k n * fact k * fact (n-k) = fact n.

Lemma comb_le_0_lt : forall k n, k <= n -> 0 < comb k n.

Lemma mult_simpl_right : forall m n p, 0 < p -> m * p = n * p -> m = n.

Corollary comb_symmetric : forall k n, k<=n -> comb k n = comb (n-k) n.

Lemma mult_lt_compat_l : forall n m p : nat, n < m -> 0 < p -> p * n < p * m.

Lemma comb_monotonic_k : forall k n k', 0<n -> k<=k' -> 2*k'<=n -> comb k n <= comb k' n.

Lemma comb_monotonic_n : forall k n n', k<=n -> n<=n' -> comb k n <= comb k n'.

Lemma comb_monotonic :
  forall k n k' n', 0<n -> k<=n -> k<=k' -> 2*k'<=n' -> n<=n' -> comb k n <= comb k' n'.

Lemma comb_max_half : forall k n, comb k n <= comb (Div2.div2 n) n.