theorem :: NEWTON06:7

for a being positive Real
for n being Nat holds [\(n * a)/] >= n * [\a/]