[Coq] itoa in Coq

https://github.com/tmiya/coq/blob/master/Radix/Radix.v

自然数$n$を$p \ge 2$で割って余りを求め、商をまた割って、と繰り返すことで$n$の$p$進表示を得られますが、そのencode/decodeをCoqで書きました。勿論、encodeとdecodeが逆関数になっていることも証明済みです。
encode関数を使って、C言語にあるitoa関数を書きました。これがあれば、数字を文字列に変換出来ますからFizzBuzzもCoqで書けます。
そのうちCoq user contributionに登録しよう。