Theorem:
(defthm len-of-nat=>lebytes*-leq-width (implies (and (natp nat) (natp width)) (equal (<= (len (nat=>lebytes* nat)) width) (< nat (expt 256 width)))) :rule-classes ((:rewrite :corollary (implies (and (natp nat) (natp width)) (equal (> (len (nat=>lebytes* nat)) width) (>= nat (expt 256 width)))) :hints (("Goal" :in-theory '(not))))))