Rprod.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Compare.
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import PartSum.
Require Import Binomial.
Require Import Omega.
Local Open Scope R_scope.

TT Ak; 0<=k<=N

Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
  match N with
    | O => f O
    | S p => prod_f_R0 f p * f (S p)
  end.

Notation prod_f_SO := (fun An N => prod_f_R0 (fun n => An (S n)) N).

(**********)
Lemma prod_SO_split :
  forall (An:nat -> R) (n k:nat),
    (k < n)%nat ->
    prod_f_R0 An n =
    prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1).forall (An : nat -> R) (n k : nat),
(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
Proof.forall (An : nat -> R) (n k : nat),
(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
  intros; induction  n as [| n Hrecn].An:nat -> R
k:nat
H:(k < 0)%nat
prod_f_R0 An 0 =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (0 - k - 1)
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S n - k - 1)
  absurd (k < 0)%nat; omega.An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S n - k - 1)
  cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|omega].An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:k = n
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S n - k - 1)
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S n - k - 1)
  replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega].An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:k = n
prod_f_R0 An n * An (S n) =
prod_f_R0 An n * An (n + 1 + 0)%nat
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S n - k - 1)
  replace (n+1+0)%nat with (S n); ring.An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S n - k - 1)
  replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega].An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
prod_f_R0 An (S n) =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (S (n - k - 1))
  simpl; replace (k + S (n - k))%nat with (S n).An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
prod_f_R0 An n * An (S n) =
prod_f_R0 An k *
(prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
   (n - k - 1) * An (k + 1 + S (n - k - 1))%nat)
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
S n = (k + S (n - k))%nat
  replace (k + 1 + S (n - k - 1))%nat with (S n).An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
prod_f_R0 An n * An (S n) =
prod_f_R0 An k *
(prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
   (n - k - 1) * An (S n))
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
S n = (k + 1 + S (n - k - 1))%nat
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
S n = (k + S (n - k))%nat
  rewrite Hrecn; [ ring | assumption ].An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
S n = (k + 1 + S (n - k - 1))%nat
An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
S n = (k + S (n - k))%nat
  omega.An:nat -> R
n, k:nat
H:(k < S n)%nat
Hrecn:(k < n)%nat ->
prod_f_R0 An n =
prod_f_R0 An k *
prod_f_R0 (fun l : nat => An (k + 1 + l)%nat)
  (n - k - 1)
H0:k = n \/ (k < n)%nat
H1:(k < n)%nat
S n = (k + S (n - k))%nat
  omega.
Qed.

(**********)
Lemma prod_SO_pos :
  forall (An:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_R0 An N.forall (An : nat -> R) (N : nat),
(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
Proof.forall (An : nat -> R) (N : nat),
(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
  intros; induction  N as [| N HrecN].An:nat -> R
H:forall n : nat, (n <= 0)%nat -> 0 <= An n
0 <= prod_f_R0 An 0
An:nat -> R
N:nat
H:forall n : nat, (n <= S N)%nat -> 0 <= An n
HrecN:(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
0 <= prod_f_R0 An (S N)
  simpl; apply H; trivial.An:nat -> R
N:nat
H:forall n : nat, (n <= S N)%nat -> 0 <= An n
HrecN:(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
0 <= prod_f_R0 An (S N)
  simpl; apply Rmult_le_pos.An:nat -> R
N:nat
H:forall n : nat, (n <= S N)%nat -> 0 <= An n
HrecN:(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
0 <= prod_f_R0 An N
An:nat -> R
N:nat
H:forall n : nat, (n <= S N)%nat -> 0 <= An n
HrecN:(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
0 <= An (S N)
  apply HrecN; intros; apply H; apply le_trans with N;
    [ assumption | apply le_n_Sn ].An:nat -> R
N:nat
H:forall n : nat, (n <= S N)%nat -> 0 <= An n
HrecN:(forall n : nat, (n <= N)%nat -> 0 <= An n) ->
0 <= prod_f_R0 An N
0 <= An (S N)
  apply H; apply le_n.
Qed.

(**********)
Lemma prod_SO_Rle :
  forall (An Bn:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
    prod_f_R0 An N <= prod_f_R0 Bn N.forall (An Bn : nat -> R) (N : nat),
(forall n : nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
Proof.forall (An Bn : nat -> R) (N : nat),
(forall n : nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
  intros; induction  N as [| N HrecN].An, Bn:nat -> R
H:forall n : nat, (n <= 0)%nat -> 0 <= An n <= Bn n
prod_f_R0 An 0 <= prod_f_R0 Bn 0
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An (S N) <= prod_f_R0 Bn (S N)
  elim  H with O; trivial.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An (S N) <= prod_f_R0 Bn (S N)
  simpl; apply Rle_trans with (prod_f_R0 An N * Bn (S N)).An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N * An (S N) <= prod_f_R0 An N * Bn (S N)
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N * Bn (S N) <= prod_f_R0 Bn N * Bn (S N)
  apply Rmult_le_compat_l.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
0 <= prod_f_R0 An N
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
An (S N) <= Bn (S N)
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N * Bn (S N) <= prod_f_R0 Bn N * Bn (S N)
  apply prod_SO_pos; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
    assumption.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
An (S N) <= Bn (S N)
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N * Bn (S N) <= prod_f_R0 Bn N * Bn (S N)
  elim (H (S N) (le_n (S N))); intros; assumption.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N * Bn (S N) <= prod_f_R0 Bn N * Bn (S N)
  do 2 rewrite <- (Rmult_comm (Bn (S N))); apply Rmult_le_compat_l.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
0 <= Bn (S N)
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N <= prod_f_R0 Bn N
  elim (H (S N) (le_n (S N))); intros.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
H0:0 <= An (S N)
H1:An (S N) <= Bn (S N)
0 <= Bn (S N)
An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N <= prod_f_R0 Bn N
  apply Rle_trans with (An (S N)); assumption.An, Bn:nat -> R
N:nat
H:forall n : nat,
(n <= S N)%nat -> 0 <= An n <= Bn n
HrecN:(forall n : nat,
 (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_R0 An N <= prod_f_R0 Bn N
prod_f_R0 An N <= prod_f_R0 Bn N
  apply HrecN; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
    split; assumption.
Qed.

Application to factorial

Lemma fact_prodSO :
  forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat =>
     (match (eq_nat_dec k 0) with
          | left   _ => 1%R
          | right _ => INR k
                        end)) n.forall n : nat,
INR (fact n) =
prod_f_R0
  (fun k : nat => if Nat.eq_dec k 0 then 1 else INR k)
  n
Proof.forall n : nat,
INR (fact n) =
prod_f_R0
  (fun k : nat => if Nat.eq_dec k 0 then 1 else INR k)
  n
  intro; induction  n as [| n Hrecn].INR (fact 0) =
prod_f_R0
  (fun k : nat => if Nat.eq_dec k 0 then 1 else INR k)
  0
n:nat
Hrecn:INR (fact n) =
prod_f_R0
  (fun k : nat =>
   if Nat.eq_dec k 0 then 1 else INR k) n
INR (fact (S n)) =
prod_f_R0
  (fun k : nat => if Nat.eq_dec k 0 then 1 else INR k)
  (S n)
  reflexivity.n:nat
Hrecn:INR (fact n) =
prod_f_R0
  (fun k : nat =>
   if Nat.eq_dec k 0 then 1 else INR k) n
INR (fact (S n)) =
prod_f_R0
  (fun k : nat => if Nat.eq_dec k 0 then 1 else INR k)
  (S n)
  simpl; rewrite <- Hrecn.n:nat
Hrecn:INR (fact n) =
prod_f_R0
  (fun k : nat =>
   if Nat.eq_dec k 0 then 1 else INR k) n
INR (fact n + n * fact n) =
INR (fact n) *
match n with
| 0%nat => 1
| S _ => INR n + 1
end
  case n; auto with real.n:nat
Hrecn:INR (fact n) =
prod_f_R0
  (fun k : nat =>
   if Nat.eq_dec k 0 then 1 else INR k) n
forall n0 : nat,
INR (fact (S n0) + S n0 * fact (S n0)) =
INR (fact (S n0)) * (INR (S n0) + 1)
  intros; repeat rewrite plus_INR;rewrite mult_INR;ring.
Qed.

Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat.forall n : nat, (n <= 2 * n)%nat
Proof.forall n : nat, (n <= 2 * n)%nat
  simple induction n.n:nat
(0 <= 2 * 0)%nat
n:nat
forall n0 : nat,
(n0 <= 2 * n0)%nat -> (S n0 <= 2 * S n0)%nat
  replace (2 * 0)%nat with 0%nat; [ apply le_n | ring ].n:nat
forall n0 : nat,
(n0 <= 2 * n0)%nat -> (S n0 <= 2 * S n0)%nat
  intros; replace (2 * S n0)%nat with (S (S (2 * n0))).n, n0:nat
H:(n0 <= 2 * n0)%nat
(S n0 <= S (S (2 * n0)))%nat
n, n0:nat
H:(n0 <= 2 * n0)%nat
S (S (2 * n0)) = (2 * S n0)%nat
  apply le_n_S; apply le_S; assumption.n, n0:nat
H:(n0 <= 2 * n0)%nat
S (S (2 * n0)) = (2 * S n0)%nat
  replace (S (S (2 * n0))) with (2 * n0 + 2)%nat; [ idtac | ring ].n, n0:nat
H:(n0 <= 2 * n0)%nat
(2 * n0 + 2)%nat = (2 * S n0)%nat
  replace (S n0) with (n0 + 1)%nat; [ idtac | ring ].n, n0:nat
H:(n0 <= 2 * n0)%nat
(2 * n0 + 2)%nat = (2 * (n0 + 1))%nat
  ring.
Qed.

We prove that (N!)^2<=(2N-k)!*k! forall k in |O;2N|

Lemma RfactN_fact2N_factk :
  forall N k:nat,
    (k <= 2 * N)%nat ->
    Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k).forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
Proof.forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
  assert (forall (n:nat), 0 <= (if eq_nat_dec n 0 then 1 else INR n)).forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
  intros; case (eq_nat_dec n 0); auto with real.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
  assert (forall (n:nat), (0 < n)%nat ->
     (if eq_nat_dec n 0 then 1 else INR n) = INR n).H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
  intros n; case (eq_nat_dec n 0); auto with real.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
n:nat
n = 0%nat -> (0 < n)%nat -> 1 = INR n
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
  intros; absurd (0 < n)%nat; omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
forall N k : nat,
(k <= 2 * N)%nat ->
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
  intros; unfold Rsqr; repeat rewrite fact_prodSO.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
  cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat).H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat ->
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  intro H2; elim H2; intro H3.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H2:k = N \/ (k < N)%nat \/ (N < k)%nat
H3:k = N
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H2:k = N \/ (k < N)%nat \/ (N < k)%nat
H3:(k < N)%nat \/ (N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega].H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H2:k = N \/ (k < N)%nat \/ (N < k)%nat
H3:(k < N)%nat \/ (N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  case H3; intro; clear H2 H3.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N).H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat => if Nat.eq_dec l 0 then 1 else INR l)
  N *
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (2 * N - k - N - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite Rmult_assoc; apply Rmult_le_compat_l.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
0 <=
prod_f_R0
  (fun l : nat => if Nat.eq_dec l 0 then 1 else INR l)
  N
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (2 * N - k - N - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply prod_SO_pos; intros; auto.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (2 * N - k - N - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  replace (2 * N - k - N-1)%nat with (N - k-1)%nat.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (N - k - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite Rmult_comm; rewrite (prod_SO_split
        (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) N k).H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun l : nat => if Nat.eq_dec l 0 then 1 else INR l)
  k *
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (k + 1 + l) 0
   then 1
   else INR (k + 1 + l)) (N - k - 1) <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k *
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (N - k - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply Rmult_le_compat_l.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
0 <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (k + 1 + l) 0
   then 1
   else INR (k + 1 + l)) (N - k - 1) <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (N - k - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply prod_SO_pos; intros; auto.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (k + 1 + l) 0
   then 1
   else INR (k + 1 + l)) (N - k - 1) <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (N - k - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply prod_SO_Rle; intros; split; auto.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(if Nat.eq_dec (k + 1 + n) 0
 then 1
 else INR (k + 1 + n)) <=
(if Nat.eq_dec (N + 1 + n) 0
 then 1
 else INR (N + 1 + n))
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite H0.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
INR (k + 1 + n) <=
(if Nat.eq_dec (N + 1 + n) 0
 then 1
 else INR (N + 1 + n))
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(0 < k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite H0.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
INR (k + 1 + n) <= INR (N + 1 + n)
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(0 < N + 1 + n)%nat
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(0 < k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply le_INR; omega.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(0 < N + 1 + n)%nat
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(0 < k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
n:nat
H2:(n <= N - k - 1)%nat
(0 < k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  assumption.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N - k - 1)%nat = (2 * N - k - N - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(k < N)%nat
(N < 2 * N - k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) k
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat =>
          if eq_nat_dec l 0 then 1 else INR l) k));
    rewrite (prod_SO_split (fun l:nat =>
          if eq_nat_dec l 0 then 1 else INR l) k N).H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat => if Nat.eq_dec l 0 then 1 else INR l)
  N *
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite Rmult_assoc; apply Rmult_le_compat_l.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
0 <=
prod_f_R0
  (fun l : nat => if Nat.eq_dec l 0 then 1 else INR l)
  N
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply prod_SO_pos; intros; auto.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) N <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1) *
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite Rmult_comm;
    rewrite (prod_SO_split (fun l:nat =>
          if eq_nat_dec l 0 then 1 else INR l) N (2 * N - k)).H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun l : nat => if Nat.eq_dec l 0 then 1 else INR l)
  (2 * N - k) *
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (2 * N - k + 1 + l) 0
   then 1
   else INR (2 * N - k + 1 + l)) (N - (2 * N - k) - 1) <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k) *
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply Rmult_le_compat_l.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
0 <=
prod_f_R0
  (fun k0 : nat =>
   if Nat.eq_dec k0 0 then 1 else INR k0) (2 * N - k)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (2 * N - k + 1 + l) 0
   then 1
   else INR (2 * N - k + 1 + l)) (N - (2 * N - k) - 1) <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply prod_SO_pos; intros; auto.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (2 * N - k + 1 + l) 0
   then 1
   else INR (2 * N - k + 1 + l)) (N - (2 * N - k) - 1) <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  replace (N - (2 * N - k)-1)%nat with (k - N-1)%nat.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (2 * N - k + 1 + l) 0
   then 1
   else INR (2 * N - k + 1 + l)) (k - N - 1) <=
prod_f_R0
  (fun l : nat =>
   if Nat.eq_dec (N + 1 + l) 0
   then 1
   else INR (N + 1 + l)) (k - N - 1)
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply prod_SO_Rle; intros; split; auto.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(if Nat.eq_dec (2 * N - k + 1 + n) 0
 then 1
 else INR (2 * N - k + 1 + n)) <=
(if Nat.eq_dec (N + 1 + n) 0
 then 1
 else INR (N + 1 + n))
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite H0.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
INR (2 * N - k + 1 + n) <=
(if Nat.eq_dec (N + 1 + n) 0
 then 1
 else INR (N + 1 + n))
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(0 < 2 * N - k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  rewrite H0.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
INR (2 * N - k + 1 + n) <= INR (N + 1 + n)
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(0 < N + 1 + n)%nat
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(0 < 2 * N - k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  apply le_INR; omega.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(0 < N + 1 + n)%nat
H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(0 < 2 * N - k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n0 : nat,
0 <= (if Nat.eq_dec n0 0 then 1 else INR n0)
H0:forall n0 : nat,
(0 < n0)%nat ->
(if Nat.eq_dec n0 0 then 1 else INR n0) = INR n0
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
n:nat
H2:(n <= k - N - 1)%nat
(0 < 2 * N - k + 1 + n)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(k - N - 1)%nat = (N - (2 * N - k) - 1)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(2 * N - k < N)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
H4:(N < k)%nat
(N < k)%nat
H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  assumption.H:forall n : nat,
0 <= (if Nat.eq_dec n 0 then 1 else INR n)
H0:forall n : nat,
(0 < n)%nat ->
(if Nat.eq_dec n 0 then 1 else INR n) = INR n
N, k:nat
H1:(k <= 2 * N)%nat
k = N \/ (k < N)%nat \/ (N < k)%nat
  omega.
Qed.


(**********)
Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n).forall n : nat, 0 < INR (fact n)
Proof.forall n : nat, 0 < INR (fact n)
  intro; apply lt_INR_0; apply neq_O_lt; red; intro;
    elim (fact_neq_0 n); symmetry ; assumption.
Qed.

We have the following inequality : (C 2N k) <= (C 2N N) forall k in |O;2N|

Lemma C_maj : forall N k:nat, (k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N.forall N k : nat,
(k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N
Proof.forall N k : nat,
(k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N
  intros; unfold C; unfold Rdiv; apply Rmult_le_compat_l.N, k:nat
H:(k <= 2 * N)%nat
0 <= INR (fact (2 * N))
N, k:nat
H:(k <= 2 * N)%nat
/ (INR (fact k) * INR (fact (2 * N - k))) <=
/ (INR (fact N) * INR (fact (2 * N - N)))
  apply pos_INR.N, k:nat
H:(k <= 2 * N)%nat
/ (INR (fact k) * INR (fact (2 * N - k))) <=
/ (INR (fact N) * INR (fact (2 * N - N)))
  replace (2 * N - N)%nat with N.N, k:nat
H:(k <= 2 * N)%nat
/ (INR (fact k) * INR (fact (2 * N - k))) <=
/ (INR (fact N) * INR (fact N))
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  apply Rmult_le_reg_l with (INR (fact N) * INR (fact N)).N, k:nat
H:(k <= 2 * N)%nat
0 < INR (fact N) * INR (fact N)
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) *
/ (INR (fact k) * INR (fact (2 * N - k))) <=
INR (fact N) * INR (fact N) *
/ (INR (fact N) * INR (fact N))
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  apply Rmult_lt_0_compat; apply INR_fact_lt_0.N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) *
/ (INR (fact k) * INR (fact (2 * N - k))) <=
INR (fact N) * INR (fact N) *
/ (INR (fact N) * INR (fact N))
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  rewrite <- Rinv_r_sym.N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) *
/ (INR (fact k) * INR (fact (2 * N - k))) <= 1
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  rewrite Rmult_comm;
    apply Rmult_le_reg_l with (INR (fact k) * INR (fact (2 * N - k))).N, k:nat
H:(k <= 2 * N)%nat
0 < INR (fact k) * INR (fact (2 * N - k))
N, k:nat
H:(k <= 2 * N)%nat
INR (fact k) * INR (fact (2 * N - k)) *
(/ (INR (fact k) * INR (fact (2 * N - k))) *
 (INR (fact N) * INR (fact N))) <=
INR (fact k) * INR (fact (2 * N - k)) * 1
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  apply Rmult_lt_0_compat; apply INR_fact_lt_0.N, k:nat
H:(k <= 2 * N)%nat
INR (fact k) * INR (fact (2 * N - k)) *
(/ (INR (fact k) * INR (fact (2 * N - k))) *
 (INR (fact N) * INR (fact N))) <=
INR (fact k) * INR (fact (2 * N - k)) * 1
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  rewrite Rmult_1_r; rewrite <- mult_INR; rewrite <- Rmult_assoc;
    rewrite <- Rinv_r_sym.N, k:nat
H:(k <= 2 * N)%nat
1 * (INR (fact N) * INR (fact N)) <=
INR (fact k * fact (2 * N - k))
N, k:nat
H:(k <= 2 * N)%nat
INR (fact k * fact (2 * N - k)) <> 0
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  rewrite Rmult_1_l; rewrite mult_INR; rewrite (Rmult_comm (INR (fact k)));
    replace (INR (fact N) * INR (fact N)) with (Rsqr (INR (fact N))).N, k:nat
H:(k <= 2 * N)%nat
(INR (fact N))² <=
INR (fact (2 * N - k)) * INR (fact k)
N, k:nat
H:(k <= 2 * N)%nat
(INR (fact N))² = INR (fact N) * INR (fact N)
N, k:nat
H:(k <= 2 * N)%nat
INR (fact k * fact (2 * N - k)) <> 0
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  apply RfactN_fact2N_factk.N, k:nat
H:(k <= 2 * N)%nat
(k <= 2 * N)%nat
N, k:nat
H:(k <= 2 * N)%nat
(INR (fact N))² = INR (fact N) * INR (fact N)
N, k:nat
H:(k <= 2 * N)%nat
INR (fact k * fact (2 * N - k)) <> 0
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  assumption.N, k:nat
H:(k <= 2 * N)%nat
(INR (fact N))² = INR (fact N) * INR (fact N)
N, k:nat
H:(k <= 2 * N)%nat
INR (fact k * fact (2 * N - k)) <> 0
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  reflexivity.N, k:nat
H:(k <= 2 * N)%nat
INR (fact k * fact (2 * N - k)) <> 0
N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0.N, k:nat
H:(k <= 2 * N)%nat
INR (fact N) * INR (fact N) <> 0
N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  apply prod_neq_R0; apply INR_fact_neq_0.N, k:nat
H:(k <= 2 * N)%nat
N = (2 * N - N)%nat
  omega.
Qed.