theorem :: REAL_3:62

for a being Nat
for r being Real st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds
for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n