theorem :: REAL_3:57

for n being Nat
for r being Real
for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds
n1 gcd n2 = 1