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

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

def periods(+q: Nat, +b: Nat, +r: Nat, +d: Nat, bound: Shape.LE(r, b)) -> {Nat.divmod.go(Nat.add(Nat.mul(q, 1n+b), r), b, d, 0n) == (Nat.add(q, d), r) : Nat & Nat}:
  match q:
    case 0n:
      %Equal.sym(Nat & Nat, Nat.divmod.go(r, b, d, 0n), (d, Nat.add(r, 0n)), remainder(r, b, d, 0n, bound)) : {_ == (d, r) : Nat & Nat}
      %Equal.sym(Nat, Nat.add(r, 0n), r, Broadcast.add_zero(r)) : {(d, _) == (d, r) : Nat & Nat}
      {==}
    case 1n+p:
      +rest = Nat.add(Nat.mul(p, 1n+b), r)
      %Index.add_assoc(b, Nat.mul(p, 1n+b), r) : {Nat.divmod.go(1n+_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
      %Equal.sym(Nat, 1n+Nat.add(b, rest), Nat.add(b, 1n+rest), Broadcast.add_succ(b, rest)) : {Nat.divmod.go(_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
      %Broadcast.add_zero(b) : {Nat.divmod.go(Nat.add(b, 1n+rest), _, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(b, 1n+rest), Nat.add(b, 0n), d, 0n), Nat.divmod.go(1n+rest, 0n, d, Nat.add(b, 0n)), drain(b, 1n+rest, 0n, d, 0n)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
      %Equal.sym(Nat, Nat.add(b, 0n), b, Broadcast.add_zero(b)) : {Nat.divmod.go(1n+rest, 0n, d, _) == (1n+Nat.add(p, d), r) : Nat & Nat}
      %Equal.sym(Nat & Nat, Nat.divmod.go(rest, b, 1n+d, 0n), (Nat.add(p, 1n+d), r), periods(p, b, r, 1n+d, bound)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
      %Broadcast.add_succ(p, d) : {(_, r) == (1n+Nat.add(p, d), r) : Nat & Nat}
      {==}

Uses (13):
  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=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_succ
  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=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=drain
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=remainder