theorem :: NEWTON07:80

for n, k being non zero Nat holds (Hartr n) . k = 1 / (n * ((n - 1) choose (k - 1)))