let n be odd Nat; :: thesis: n choose ((n + 1) / 2) = n choose ((n - 1) / 2)
reconsider k = (n - 1) / 2 as Nat ;
(k + (k + 1)) choose k = (k + (k + 1)) choose (k + 1) by N20;
hence n choose ((n + 1) / 2) = n choose ((n - 1) / 2) ; :: thesis: verum