let n be Nat; :: thesis: for r being Real holds (c_d r) . n >= 0
let r be Real; :: thesis: (c_d r) . n >= 0
set s = scf r;
set s1 = c_d r;
defpred S2[ Nat] means (c_d r) . $1 >= 0 ;
A1: for n being Nat st S2[n] & S2[n + 1] holds
S2[n + 2]
proof
let n be Nat; :: thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] )
assume A2: (c_d r) . n >= 0 ; :: thesis: ( not S2[n + 1] or S2[n + 2] )
A3: (c_d r) . (n + 2) = (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n) by Def6;
n + 2 > 1 + 0 by XREAL_1:8;
then A4: (scf r) . (n + 2) >= 0 by Th38;
assume (c_d r) . (n + 1) >= 0 ; :: thesis: S2[n + 2]
hence S2[n + 2] by A4, A3, A2; :: thesis: verum
end;
(scf r) . 1 >= 0 by Th38;
then A5: S2[1] by Def6;
A6: S2[ 0 ] by Def6;
for n being Nat holds S2[n] from FIB_NUM:sch 1(A6, A5, A1);
 hence (c_d r) . n >= 0 ; :: thesis: verum