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