let n be natural number ; :: thesis: ( n > 1 implies Catalan n < Catalan (n + 1) )
set a = ((2 * n) -' 2) ! ;
set b = (2 * n) ! ;
A1: Catalan (n + 1) = ((2 * n) ! ) / ((n ! ) * ((n + 1) ! )) by Th14;
assume A2: n > 1 ; :: thesis: Catalan n < Catalan (n + 1)
then (n -' 1) + 1 = n by XREAL_1:237;
then A3: (((((2 * n) -' 2) ! ) * n) * (n + 1)) / ((n ! ) * ((n + 1) ! )) = (((((2 * n) -' 2) ! ) * n) * (n + 1)) / ((n * ((n -' 1) ! )) * ((n + 1) ! )) by NEWTON:21
.= (n * ((((2 * n) -' 2) ! ) * (n + 1))) / (n * (((n -' 1) ! ) * ((n + 1) ! )))
.= ((((2 * n) -' 2) ! ) * (n + 1)) / (((n -' 1) ! ) * ((n + 1) ! )) by A2, XCMPLX_1:92
.= ((((2 * n) -' 2) ! ) * (n + 1)) / (((n -' 1) ! ) * ((n + 1) * (n ! ))) by NEWTON:21
.= ((((2 * n) -' 2) ! ) * (n + 1)) / ((((n -' 1) ! ) * (n ! )) * (n + 1))
.= (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! )) by XCMPLX_1:92 ;
( n ! > 0 & (n + 1) ! > 0 ) by NEWTON:23;
then (n ! ) * ((n + 1) ! ) > 0 * (n ! ) by XREAL_1:70;
then (((((2 * n) -' 2) ! ) * n) * (n + 1)) / ((n ! ) * ((n + 1) ! )) < ((2 * n) ! ) / ((n ! ) * ((n + 1) ! )) by A2, Th6, XREAL_1:76;
hence Catalan n < Catalan (n + 1) by A2, A1, A3, Th8; :: thesis: verum