>>518-519
Coqでは止まらない再帰関数は書けないので、
>>373では、再帰を有限回で0終了させる引数yを入れてあります。
で、どんなxに対してもlast collatz03が0にならないyが存在する、という事で、
Require Import List.して

Theorem collatz_is_true:
forall (x:nat), x<>0 -> (exists y:nat, 1=(last (collatz03 x y) 0)).

ってとこじゃないでしょうか。