let n be Nat; :: thesis: for r being Real holds (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1))
let r be Real; :: thesis: (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1))
set s = scf r;
set s1 = c_d r;
set m = ((scf r) . (n + 2)) * ((c_d r) . (n + 1));
((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by Def6;
then ((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) >= 0 by Th51;
then (((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1)))) + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) >= 0 + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by XREAL_1:6;
hence (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) ; :: thesis: verum