>>140
このライブラリを使えばいいんじゃないかな、
https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html

nステップ以下で停止するって述語が
Hypothesis P_dec : forall n, {P n}+{~(P n)}.
を満たしていれば、停止するステップ数を構成してくれるよ。