fact: Fixpoint show_uint (n : uint) : string := match n with | Nil => "" | D0 n => String "0" (show_uint n) | D1 n => String "1" (show_uint n) | D2 n => String "2" (show_uint n) | D3 n => String "3" (show_uint n) | D4 n => String "4" (show_uint n) | D5 n => String "5" (show_uint n) | D6 n => String "6" (show_uint n) | D7 n => String "7" (show_uint n) | D8 n => String "8" (show_uint n) | D9 n => String "9" (show_uint n) end.
imports: Coq(Ascii Basics Decimal List String ZArith)