theorem Th31: :: PREPOWER:31

for a being Real
for n being Nat st a > 0 & n >= 1 holds
(n -Root a) - 1 <= (a - 1) / n