theorem :: NAT_2:20

for k, n being Nat st n <= k & k < n + n holds
k div n = 1