law signed_bound_last_inside

bendtorch-core@0.1.0.0 · src/tensor/signed_LAWS.bend:334

import Base
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed

334law signed_bound_last_inside:
335  for +limit: U32
336  for +k: U32
337  for inside: {U32.is_lt(k, limit) == True{} : Bool}
338  {Nat.add(U32.to_nat(Signed.bound(limit, Signed.Last{k})), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}