U32.internal_u32_to_nat_from_nat: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 691-699 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=691&end_line=699

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

def internal_u32_to_nat_from_nat(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat, h: MNat.lt(k, m)) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}:
  match k:
    case 0n:
      {==}
    case 1n++p:
      +h = h
      +ih = internal_u32_to_nat_from_nat(m, e, p, MNat.lt_trans(p, 1n+p, m, MNat.lt_succ_self(p), h))
      +hu = internal_lt_congl(1n+p, 1n+U32.to_nat(U32.from_nat(p)), m, Equal.cong(Nat, Nat, z => 1n+z, p, U32.to_nat(U32.from_nat(p)), Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ih)), h)
      Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p, internal_u32_inc_exact(m, U32.from_nat(p), e, hu), Equal.cong(Nat, Nat, z => 1n+z, U32.to_nat(U32.from_nat(p)), p, ih))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt_succ_self
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_lt_congl
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_u32_inc_exact