NatOrder.digit_bounded: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder
Lines 267-270 of stelliferous@0.0.2.0/proofs/nat_order.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&start_line=267&end_line=270

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

def digit_bounded(+a: Nat,+b: Nat,+bit: Bool,+cap: Nat,small: {Nat.is_lt(a,b) == True{} : Bool},large: {Nat.is_le(Nat.double(b),
      cap) == True{} : Bool}) -> {Nat.is_le(Comparison.digit(bit,a),cap) == True{} : Bool}:
  Bounds.strict_le(Comparison.digit(bit,a),cap,Bounds.nat_trans(Comparison.digit(bit,a),Nat.double(b),cap,digit_lt(a,b,bit,
        small),large))

Uses (9):
  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.double
  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=stelliferous@0.0.2.0/proofs/nat_order.bend&name=digit_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=nat_trans
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=strict_le
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=digit