ググれば出てきそうな気もしますが、がんばってみました。しかしあえなく轟沈。(証明どころか関数さえ書けない始末…情けない。)Coqではちゃんと停止する関数しか書けないです。これは再帰が書けないという事ではなく、再帰にはDefinitionの代わりにFixpoint…