Lemmas.u32_to_from_nat: law of bend-kit-lemmas@0.1.1.0
Import: import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas
Lines 686-689 of bend-kit-lemmas@0.1.1.0/lemmas.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&start_line=686&end_line=689

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

law u32_to_from_nat:
  for k: Nat
  for +h: MNat.lt(k, pow2(32n))
  {U32.to_nat(U32.from_nat(k)) == k : Nat}

Uses (12):
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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-kit-lemmas@0.1.1.0/lemmas.bend&name=lt_rw
  https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-kit-lemmas@0.1.1.0/lemmas.bend&name=u32_inc_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