>>328
質問の答えになっているか分からないですが、
今回の方法だと、再帰関数を書き終えた時点で証明モードに入って、そこでの証明を終えると、関数が定義されます。
具体的には、Coq.Program.Wfをインポートして、減少する引数をmeasureで指定して、Program Fixpointで関数を書きます。
https://www.google.com/url?q=http://d.hatena.ne.jp/airobo/touch/20130729/1375109706&sa=U&ved=0ahUKEwiAtI7aq_fbAhUIjpQKHc5jA0wQFggLMAA&usg=AOvVaw0Z5Y7z7Pexxi_2FgNFFFX2