def digit_bounded

stelliferous@0.0.2.0 · proofs/nat_order.bend:267

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

267def 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),
268      cap) == True{} : Bool}) -> {Nat.is_le(Comparison.digit(bit,a),cap) == True{} : Bool}:
269  Bounds.strict_le(Comparison.digit(bit,a),cap,Bounds.nat_trans(Comparison.digit(bit,a),Nat.double(b),cap,digit_lt(a,b,bit,
270        small),large))