:: by Dorota Cz\c{e}stochowska and Adam Grabowski

::

:: Received May 31, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

begin

:: deftheorem defines Catalan CATALAN1:def 1 :

for n being Nat holds Catalan n = (((2 * n) -' 2) choose (n -' 1)) / n;

for n being Nat holds Catalan n = (((2 * n) -' 2) choose (n -' 1)) / n;

theorem Th9: :: CATALAN1:9

for n being Nat st n > 1 holds

Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))

Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))

proof end;

registration
end;

registration
end;