SlicePROOF.div_step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
Lines 729-734 of bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&start_line=729&end_line=734

import Base
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedProof

# (k * step) / step = k for a positive step.
def div_step(+k: Nat, +step: Nat, +positive: {Nat.is_lt(0n, step) == True{} : Bool}) -> {Nat.div(Nat.mul(k, step), step) == k : Nat}:
  Equal.trans(Nat, Nat.div(Nat.mul(k, step), step), Nat.div(Nat.add(Nat.mul(k, step), 0n), step), k,
    Equal.cong(Nat, Nat, x => Nat.div(x, step), Nat.mul(k, step), Nat.add(Nat.mul(k, step), 0n),
      Equal.sym(Nat, Nat.add(Nat.mul(k, step), 0n), Nat.mul(k, step), add_zero_right(Nat.mul(k, step)))),
    BatchedProof.div_exact(k, step, 0n, positive))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=div_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=add_zero_right