SlicePROOF.reaches_span: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
Lines 214-223 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=214&end_line=223

import Base
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts

def reaches_span(+start: Nat, +stop: Nat, +step: Nat, +span: Nat, e: {Nat.sub(stop, start) == span : Nat},
  positive: {Nat.is_lt(0n, step) == True{} : Bool}) ->
  {Nat.is_le(stop, Nat.add(start, Nat.mul(Slice.counted(span, step), step))) == True{} : Bool}:
  match span:
    case 0n:
      %Equal.sym(Nat, Nat.add(start, 0n), start, add_zero_right(start)) : {Nat.is_le(stop, _) == True{} : Bool}
      sub_zero_le(stop, start, e)
    case 1n+rest:
      %sub_back(stop, start, rest, e) : {Nat.is_le(_, Nat.add(start, Nat.mul(1n+Nat.div(rest, step), step))) == True{} : Bool}
      Facts.le_add_cong(start, 1n+rest, Nat.add(step, Nat.mul(Nat.div(rest, step), step)), cover(rest, step, positive))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_le
  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=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=le_add_cong
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=counted
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=add_zero_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=cover
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=sub_back
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=sub_zero_le