U32.internal_wrap_sum: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 840-843 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=840&end_line=843

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

def internal_wrap_sum(+b: Nat, +s: Nat, +m: Nat, -v: Nat, hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}) -> {Nat.add(b, Nat.add(s, Nat.sub(m, b))) == v : Nat}:
  %MNat.add_left_comm(s, b, Nat.sub(m, b)) : {_ == v : Nat}
  %Equal.sym(Nat, Nat.add(b, Nat.sub(m, b)), m, MNat.add_sub_of_le(b, m, MNat.le_of_lt(b, m, hb))) : {Nat.add(s, _) == v : Nat}
  es

Uses (8):
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_left_comm
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_sub_of_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt