def mod_exact
bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:339
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
339def mod_exact(+q: Nat, +b: Nat, +r: Nat, below: {Nat.is_lt(r, b) == True{} : Bool}) -> {Nat.mod(Nat.add(Nat.mul(q, b), r), b) == r : Nat}:
340 Equal.cong(Nat & Nat, Nat, pair => Pair.snd(Nat, Nat, pair), Nat.divmod(Nat.add(Nat.mul(q, b), r), b), (q, r),
341 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))))