def divmod_exact

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:153

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

153def 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}:
154  match b:
155    case 0n:
156      Empty.absurd({(q, r) == Nat.divmod(Nat.add(Nat.mul(q, 0n), r), 0n) : Nat & Nat}, lt_zero(r, bound))
157    case 1n+p:
158      %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}
159      %Equal.sym(Nat, Nat.add(q, 0n), q, Broadcast.add_zero(q)) : {(q, r) == (_, r) : Nat & Nat}
160      {==}