WordArithmetic.native_encoding: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
Lines 118-120 of stelliferous@0.0.2.0/proofs/word_arithmetic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&start_line=118&end_line=120

import Base

law native_encoding:
  for +a: Nat
  {U32.from_nat(a) == U32{encode(a,32n)} : U32}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=encode