SignedPROOF.last_below: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF
Lines 115-126 of bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&start_line=115&end_line=126

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

# In range, limit - 1 - k is below limit.
def last_below(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
  {U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit) == True{} : Bool}:
  Equal.trans(Bool, U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit), Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)), True{},
    Equal.sym(Bool, Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)), U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit),
      Arith.u32_lt(U32.sub(U32.sub(limit, 1), k), limit)),
    Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)),
      Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k))), True{},
      Equal.cong(Nat, Bool, x => Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), x), U32.to_nat(limit),
        Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)),
        Equal.sym(Nat, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)), U32.to_nat(limit), last_inside(limit, k, inside))),
      lt_past(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k))))

Uses (14):
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=u32_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=last_inside
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=lt_past