def word_below
bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:86
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
import Base
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
86def word_below(+number: Nat, +limit: U32, below: {Nat.is_lt(number, U32.to_nat(limit)) == True{} : Bool}) ->
87 {U32.to_nat(U32.from_nat(number)) == number : Nat}:
88 Conversion.natural_word_exact(number, limit, Conversion.lt_le(number, U32.to_nat(limit), below))