NatProofs.divmod_exact: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs
Lines 153-160 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=153&end_line=160

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 divmod_exact(+q: Nat, +b: Nat, +r: Nat, bound: Shape.LT(r, b)) -> {(q, r) == Nat.divmod(Nat.add(Nat.mul(q, b), r), b) : Nat & Nat}:
  match b:
    case 0n:
      Empty.absurd({(q, r) == Nat.divmod(Nat.add(Nat.mul(q, 0n), r), 0n) : Nat & Nat}, lt_zero(r, bound))
    case 1n+p:
      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(Nat.mul(q, 1n+p), r), p, 0n, 0n), (Nat.add(q, 0n), r), periods(q, p, r, 0n, lt_le(r, p, bound))) : {(q, r) == _ : Nat & Nat}
      %Equal.sym(Nat, Nat.add(q, 0n), q, Broadcast.add_zero(q)) : {(q, r) == (_, r) : Nat & Nat}
      {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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
  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=Nat.mul
  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_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LT
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=lt_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=periods