let r be Real; :: thesis:
set s = scf r;
set s1 = c_d r;
defpred S₂[ Nat] means ((c_d r) . ($1 + 1)) / ((c_d r) . $1) >= 1 / ((scf r) . ($1 + 2));
assume A1: for n being Nat holds (scf r) . n > 0 ; :: thesis:
then A2: (scf r) . 1 <> 0 ;
A3: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis:
assume ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ; :: thesis:
set r = (c_d r) . (n + 1);
A4: (scf r) . 1 > 0 by A1;
then A5: (c_d r) . (n + 1) > 0 by Th52;
( n + 3 >= 0 + 1 & (scf r) . (n + 3) <> 0 ) by A1, XREAL_1:7;
then (scf r) . (n + 3) >= 1 by Th40;
then A6: 1 / ((scf r) . (n + 3)) <= 1 / 1 by XREAL_1:118;
( n + 2 >= 0 + 1 & (scf r) . (n + 2) <> 0 ) by A1, XREAL_1:7;
then A7: (scf r) . (n + 2) >= 1 by Th40;
A8: (c_d r) . n > 0 by A4, Th52;
((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) / ((c_d r) . (n + 1)) by Def6
.= ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) / ((c_d r) . (n + 1))) + (((c_d r) . n) / ((c_d r) . (n + 1)))
.= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) / ((c_d r) . (n + 1)))) + (((c_d r) . n) / ((c_d r) . (n + 1)))
.= ((scf r) . (n + 2)) + (((c_d r) . n) / ((c_d r) . (n + 1))) by A5, XCMPLX_1:88 ;
then ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) >= 1 + 0 by A5, A8, A7, XREAL_1:7;
hence S₂[n + 1] by A6, XXREAL_0:2; :: thesis:

end;

(scf r) . 2 <> 0 by A1;
then (scf r) . (0 + 2) >= 1 by Th40;
then A9: 1 / ((scf r) . (0 + 2)) <= 1 / 1 by XREAL_1:118;
( (c_d r) . 0 = 1 & (c_d r) . 1 = (scf r) . 1 ) by Def6;
then ((c_d r) . (0 + 1)) / ((c_d r) . 0) >= 1 by A2, Th40;
then A10: S₂[ 0 ] by A9, XXREAL_0:2;
for n being Nat holds S₂[n] from NAT_1:sch 2(A10, A3);
hence for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ; :: thesis: