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