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