Library Coq.Reals.Rprod
TT Ak; 0<=k<=N
Application to factorial
We prove that (N!)^2<=(2N-k)!*k! forall k in |O;2N|
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.