theorem :: DIOPHAN1:19

for n being Nat
for r being Real st r is irrational holds
(c_d r) . (n + 2) >= 2 * ((c_d r) . n)