"value <= 256^byteCount", as (value - 1) < 256^byteCount with the saturating
predecessor: 0 qualifies, 256^byteCount itself qualifies, one more does not.
Callers that wrote `naturalLessOrEqual x bound` keep exactly that bound.
239def naturalAtMostBytePower =
240 (lambda unrestricted byteCount : Nat .
241 (lambda unrestricted value : Nat . (naturalBelowBytePower byteCount (naturalPredecessor value))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.