>>600
定義するなら、n_0 に最小性の条件を課して、
n_0 を決定番号扱いすれば記事が短くなるんじゃないか。