theorem FOTN: :: MOEBIUS2:4

for a, n being non zero Nat holds (n div a) * a <= n