剰余コラッツ予想の例のプログラムですが、
Coqに移植できました。

Coqの関数は全て停止するので、例のプログラムも停止する事になって、
『剰余コラッツ予想は真！』
……と言いたいところですが、怪しさ満載ですので、今しばらく調査します。