ProofSame.tl_dec: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_same.bend as ProofSame
Lines 265-271 of lawful-bytes@0.1.1.0/proof_same.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_same.bend&start_line=265&end_line=271

import Base

# j - 1 for j = 1 + m + s.
law tl_dec:
  for +m: Nat
  for +s: U32
  for +j: U32
  for +hj: {U32.to_nat(j) == 1n+Nat.add(m, U32.to_nat(s)) : Nat}
  {U32.to_nat((j - 1 : U32)) == Nat.add(m, U32.to_nat(s)) : Nat}

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_zero_l
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=sub_zero
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_le_to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_sub_le