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