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