theorem Th29: :: CATALAN2:29

for m, n being Nat st 2 * m <= n holds
card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)