(n mod (m + 1)) choose ((m + 1) - 1) < 2 by NPP;
then ( (n mod (m + 1)) choose m = 0 or (n mod (m + 1)) choose m = 1 ) by NAT_1:23;
hence (n mod (m + 1)) choose m is trivial by NAT_2:def 1; :: thesis: verum