U32.internal_wrap_rem: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 845-850 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=845&end_line=850

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

def internal_wrap_rem(+b: Nat, +s: Nat, +m: Nat, +v: Nat, +hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}, hv: MNat.lt(v, Nat.double(b))) -> {Nat.add(b, Nat.mod(Nat.add(s, Nat.sub(m, b)), m)) == v : Nat}:
  +y = Nat.add(s, Nat.sub(m, b))
  +ey = internal_wrap_sum(b, s, m, v, hb, es)
  +hy = internal_rem_lt(b, y, v, ey, hv)
  %Equal.sym(Nat, Nat.mod(y, m), y, MNat.mod_eq_of_lt(y, m, MNat.lt_trans(y, b, m, hy, hb))) : {Nat.add(b, _) == v : Nat}
  ey

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.double
  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.sub
  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_trans
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=mod_eq_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_rem_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_wrap_sum