def capacity_within
bendtorch-core@0.1.0.0 · src/tensor/word_conversion.bend:579
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProof
579def capacity_within(+number: Nat, within: Shape.LE(number, 1048576n)) ->
580 {Nat.is_le(number, U32.to_nat(1048576)) == True{} : Bool}:
581 Equal.trans(Bool, Nat.is_le(number, U32.to_nat(1048576)), Nat.is_le(number, 1048576n), True{},
582 Equal.cong(Nat, Bool, n => Nat.is_le(number, n), U32.to_nat(1048576), 1048576n, capacity_word_nat()),
583 Equal.sym(Bool, True{}, Nat.is_le(number, 1048576n), NatProof.le_true(number, 1048576n, within)))