def div_step

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:729

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

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