let a be Real; :: thesis: for n being Nat st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
let n be Nat; :: thesis: ( a > 0 & n >= 1 implies (n -root a) - 1 <= (a - 1) / n )
assume A1: ( a > 0 & n >= 1 ) ; :: thesis: (n -root a) - 1 <= (a - 1) / n
then (n -Root a) - 1 <= (a - 1) / n by PREPOWER:31;
hence (n -root a) - 1 <= (a - 1) / n by A1, Def1; :: thesis: verum