NatProofs.remainder: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs
Lines 125-134 of bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&start_line=125&end_line=134

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

def remainder(+r: Nat, +m: Nat, -d: Nat, +a: Nat, bound: Shape.LE(r, m)) -> {Nat.divmod.go(r, m, d, a) == (d, Nat.add(r, a)) : Nat & Nat}:
  match r m:
    case 0n m:
      {==}
    case 1n+p 0n:
      match bound:
    case 1n+p 1n+q:
      %Equal.sym(Nat & Nat, Nat.divmod.go(p, q, d, 1n+a), (d, Nat.add(p, 1n+a)), remainder(p, q, d, 1n+a, bound)) : {_ == (d, 1n+Nat.add(p, a)) : Nat & Nat}
      %Broadcast.add_succ(p, a) : {(d, _) == (d, 1n+Nat.add(p, a)) : Nat & Nat}
      {==}

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.divmod.go
  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=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE