あーしかし
切断からコーシー列作るのには選択公理が必要な気がする
こんな**big picture**か

Q　→　コーシー列
‖　不用↓　　　↓不用
Q　→　切断　→ R
　　　　　　不用

Qのコーシー列から切断への自然な全射の右逆写像
けれどコーシー列や切断から作られるRは
どちらも実数の公理を満たすので同じもの