Convert a natural number to its non-empty minimum-length little-endian list of bytes, seen as sigits in base 256.
(nat=>lebytes+ nat) → digits
Function:
(defun nat=>lebytes+ (nat) (declare (xargs :guard (natp nat))) (let ((__function__ 'nat=>lebytes+)) (declare (ignorable __function__)) (nat=>lendian+ 256 nat)))
Theorem:
(defthm byte-listp-of-nat=>lebytes+ (b* ((digits (nat=>lebytes+ nat))) (byte-listp digits)) :rule-classes :rewrite)
Theorem:
(defthm nat=>lebytes+-of-nfix-nat (equal (nat=>lebytes+ (nfix nat)) (nat=>lebytes+ nat)))
Theorem:
(defthm nat=>lebytes+-nat-equiv-congruence-on-nat (implies (nat-equiv nat nat-equiv) (equal (nat=>lebytes+ nat) (nat=>lebytes+ nat-equiv))) :rule-classes :congruence)