let n be Nat; :: thesis: Catalan n <= Catalan (n + 1)

per cases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25;

suppose n = 0 ; :: thesis: Catalan n <= Catalan (n + 1)

hence Catalan n <= Catalan (n + 1) ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: Catalan n <= Catalan (n + 1)

hence Catalan n <= Catalan (n + 1) by Th11, Th12; :: thesis: verum

end;

suppose n > 1 ; :: thesis: Catalan n <= Catalan (n + 1)

hence Catalan n <= Catalan (n + 1) by Th15; :: thesis: verum

end;

end;