let n be Nat; :: thesis: (((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2)) + ((n + 6) choose 3) = ((n + 7) choose 3) - ((n + 6) choose 1)
( n choose 0 = 1 & ((n + 1) + 1) choose 1 = n + 2 & (n + 4) choose 2 = ((n + 4) * ((n + 4) - 1)) / 2 & (n + 6) choose 3 = (((n + 6) * ((n + 6) - 1)) * ((n + 6) - 2)) / 6 & (n + 7) choose 3 = (((n + 7) * ((n + 7) - 1)) * ((n + 7) - 2)) / 6 & (n + 6) choose 1 = n + 6 ) by STIRL2_1:51, NEWTON:19;
hence (((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2)) + ((n + 6) choose 3) = ((n + 7) choose 3) - ((n + 6) choose 1) ; :: thesis: verum