Big-endian representation of scalars in RLP.
The library function nat=>bebytes*
We introduce two linear rules that relate certain specific upper bounds on numbers and their big-endian representations in base 256. These upper bounds apply to the encoding of lengths in RLP.
(defthm len-of-nat=>bebytes*-leq-8 (implies (< nat (expt 2 64)) (<= (len (nat=>bebytes* nat)) 8)) :rule-classes :linear)