m mod n < n by NAT_D:1;
hence (m mod n) choose n is zero by NEWTON:def 3; :: thesis: verum