>>739
> aとbが互いに素 ⇔ an - bc = 1となる自然数、n, c がある

この問題には「bc - an = 1」となる自然数 c,n があるのほうがよかった
ね。この n = [bc/a] で、最小の小数部は もちろん 1/a だ。0 < c < aも
証明できる (もし c > a なら c' = c-a とできる)。

上記はユークリッド互除法のひとつの表現形式だ。a, b から c, nを求める
アルゴリズムを 拡張ユークリッド互除法 という。