MatrixIndexProof.stepped_right: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
Lines 249-251 of bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&start_line=249&end_line=251

import Base
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index

def stepped_right(+columns: Nat, +column: Nat, +k: Nat) ->
  {Nat.add(columns, Nat.add(Nat.mul(k, columns), column)) == Nat.add(Nat.mul(1n+k, columns), column) : Nat}:
  Index.add_assoc(columns, Nat.mul(k, columns), column)

Uses (4):
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=add_assoc