SignedPROOF.past_bound: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF
Lines 303-307 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=303&end_line=307

import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs

# A size past the bound times a nonzero product is past the bound.
def past_bound(+bound: Nat, +less: Nat, +rest: Nat, past: {Nat.is_lt(bound, 1n+less) == True{} : Bool}) ->
  {Nat.is_le(Nat.mul(1n+less, 1n+rest), bound) == False{} : Bool}:
  %NatProofs.mul_comm(1n+rest, 1n+less) : {Nat.is_le(_, bound) == False{} : Bool}
  not_le_add(1n+less, Nat.mul(rest, 1n+less), bound, lt_not_le(bound, 1n+less, past))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=lt_not_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=not_le_add