let n be Nat; :: 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:235;
then A3: (((((2 * n) -' 2) !) * n) * (n + 1)) / ((n !) * ((n + 1) !)) = (((((2 * n) -' 2) !) * n) * (n + 1)) / ((n * ((n -' 1) !)) * ((n + 1) !)) by NEWTON:15
.= (n * ((((2 * n) -' 2) !) * (n + 1))) / (n * (((n -' 1) !) * ((n + 1) !)))
.= ((((2 * n) -' 2) !) * (n + 1)) / (((n -' 1) !) * ((n + 1) !)) by A2, XCMPLX_1:91
.= ((((2 * n) -' 2) !) * (n + 1)) / (((n -' 1) !) * ((n + 1) * (n !))) by NEWTON:15
.= ((((2 * n) -' 2) !) * (n + 1)) / ((((n -' 1) !) * (n !)) * (n + 1))
.= (((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) by XCMPLX_1:91 ;
( n ! > 0 & (n + 1) ! > 0 ) by NEWTON:17;
then (n !) * ((n + 1) !) > 0 * (n !) by XREAL_1:68;
then (((((2 * n) -' 2) !) * n) * (n + 1)) / ((n !) * ((n + 1) !)) < ((2 * n) !) / ((n !) * ((n + 1) !)) by A2, Th6, XREAL_1:74;
hence Catalan n < Catalan (n + 1) by A2, A1, A3, Th8; :: thesis: verum