let n be Nat; :: thesis: ((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2) = ((n + 5) choose 2) - ((n + 5) choose 0)
( n choose 0 = 1 & ((n + 1) + 1) choose 1 = n + 2 & ((n + 3) + 1) choose 2 = ((n + 3) * (n + 4)) / 2 & ((n + 4) + 1) choose 2 = ((n + 4) * (n + 5)) / 2 & (n + 5) choose 0 = 1 ) by NEWTON:19, NUMPOLY1:72;
hence ((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2) = ((n + 5) choose 2) - ((n + 5) choose 0) ; :: thesis: verum