~/jendhub

def div_exact

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:334

import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedMatmulPROOF
import Base
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

334# Division and remainder of q * b + r by b, for r below b.
335def div_exact(+q: Nat, +b: Nat, +r: Nat, below: {Nat.is_lt(r, b) == True{} : Bool}) -> {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}:
336  Equal.cong(Nat & Nat, Nat, pair => Pair.fst(Nat, Nat, pair), Nat.divmod(Nat.add(Nat.mul(q, b), r), b), (q, r),
337    Equal.sym(Nat & Nat, (q, r), Nat.divmod(Nat.add(Nat.mul(q, b), r), b), Nats.divmod_exact(q, b, r, MatrixIndex.lt_from(r, b, below))))

Uses (14)

Used by (9)