def past_bound

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:303

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

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