theorem :: CATALAN1:5

for n being Nat st n > 1 holds
(((4 * n) * n) - (2 * n)) / (n + 1) > 1