let n be Nat; :: thesis: ((n + 1) choose 2) - (n choose 2) = n
(n choose (1 + 1)) + (n choose 1) = (n + 1) choose (1 + 1) by NEWTON:22;
hence ((n + 1) choose 2) - (n choose 2) = n ; :: thesis: verum