Theorem:
(defthm lebytes=>nat-injectivity+ (implies (and (equal (trim-lendian+ (byte-list-fix digits1)) digits1) (equal (trim-lendian+ (byte-list-fix digits2)) digits2)) (equal (equal (lebytes=>nat digits1) (lebytes=>nat digits2)) (equal digits1 digits2))))