law show_lgo

lawful-fields@0.1.1.0 · proof_digits.bend:281

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

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