Theorems about results of std/strings functions that return lists of decimal digit characters.
Those std/strings are accompanied by theorems that they return dec-digit-char-list*p, but they in fact return true lists, so here we add theorems that they return dec-digit-char-listp.
Theorem:
(defthm dec-digit-char-listp-of-basic-nat-to-dec-chars (dec-digit-char-listp (basic-nat-to-dec-chars nat)))
Theorem:
(defthm dec-digit-char-listp-of-nat-to-dec-chars-aux (implies (dec-digit-char-listp acc) (dec-digit-char-listp (nat-to-dec-chars-aux nat acc))))
Theorem:
(defthm dec-digit-char-listp-of-nat-to-dec-chars (dec-digit-char-listp (nat-to-dec-chars nat)))