Only width32 uses the already-qualified base256 range identity.
Select functions so the unused old power expression is not evaluated.
Quotient chunks avoid constructing a power larger than one byte.
For width = 8*q+r, floor(value / 256^q) < 2^r exactly means value < 2^width.
364def sm86FieldDivideByteChunks =
365 (lambda unrestricted count : Nat .
366 (lambda unrestricted value : Nat .
367 (app
368 (nat-eliminate
369 (lambda unrestricted current : Nat . (pi unrestricted remainingValue : Nat . Nat))
370 (lambda unrestricted remainingValue : Nat . remainingValue)
371 (lambda unrestricted predecessor : Nat .
372 (lambda unrestricted induction : (pi unrestricted remainingValue : Nat . Nat) .
373 (lambda unrestricted remainingValue : Nat .
374 (induction (naturalDivideUnchecked remainingValue byteNaturalTwoHundredFiftySix)))))
375 count)
376 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.