for s, t being natural Number holds (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)