fact: Definition digit2ascii (n:nat) : Ascii.ascii := match n with | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | 9 => "9" | n => ascii_of_nat (n - 10 + nat_of_ascii "A") end%char.
imports: Coq.Strings.Ascii ExtLib.Data.Bool ExtLib.Tactics.Consider ExtLib.Core.RelDec