theorem :: REAL_3:70

for r being Real st (scf r) . 1 > 0 holds
for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n))