Catalan 1 = ((2 * 1) -' 2) choose 0 by XREAL_1:232
.= 1 by NEWTON:19 ;
hence Catalan 1 = 1 ; :: thesis: verum