for n being Nat holds Catalan n <= Catalan (n + 1)