base58-val=>char and base58-char=>val are mutual inverses.
Theorem:
(defthm base58-char=>val=>char (equal (base58-val=>char (base58-char=>val char)) (base58-character-fix char)))
Theorem:
(defthm base58-val=>char=>val (equal (base58-char=>val (base58-val=>char val)) (base58-value-fix val)))