let a, n be non zero Nat; :: thesis: (n div a) * a <= n
n = (a * (n div a)) + (n mod a) by NAT_D:2;
hence (n div a) * a <= n by NAT_1:11; :: thesis: verum