ProofDigits.show_lgo: law of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits
Lines 281-283 of lawful-fields@0.1.1.0/proof_digits.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&start_line=281&end_line=283

import Base
import lawful-fields@0.1.1.0/defs.bend as F

law show_lgo:
  for +m: Nat
  {F.codes(Nat.show(m)) == lgo(m, Nat.div(m, 10n), DG(m), Nil{}) : List<&2, U32>}

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.show
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.show.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.show.put
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=codes
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=DG
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=eta_nn
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=lgo
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=show_fin