def internal_u32_to_nat_lt

bend-mathlib@0.8.1.0 · u32.bend:503

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

503def internal_u32_to_nat_lt(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> MNat.lt(U32.to_nat(a), m):
504  match a:
505    case U32{w}:
506      %e : MNat.lt(Word.to_nat(32n, w), _)
507      word_to_nat_lt(32n, w)