theorem :: REAL_3:56

for b being Nat
for r being Real st ( for n being Nat holds (scf r) . n <= b ) holds
for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)