for n being Nat st n <> 0 holds
n div n = 1