:: deftheorem defines convergents_of_continued_fractions REAL_3:def 7 :
for r being Real holds convergents_of_continued_fractions r = (c_n r) /" (c_d r);