:: deftheorem defines Catalan CATALAN1:def 1 :
for n being Nat holds Catalan n = (((2 * n) -' 2) choose (n -' 1)) / n;