Below.acc_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as Below
Lines 89-95 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend&start_line=89&end_line=95

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR

def acc_lt(+h: Nat, +k: Nat, +n: Nat, +hh: {Nat.is_lt(h, n) == True{} : Bool}, +ok: Bool, +e: {SR.accept(h, ok) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_lt(k, n) == True{} : Bool}:
  match ok:
    case True{}:
      %some_inj(h, k, e) : {Nat.is_lt(_, n) == True{} : Bool}
      hh
    case False{}:
      Empty.absurd({Nat.is_lt(k, n) == True{} : Bool}, none_some(k, e))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend&name=none_some
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend&name=some_inj
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend&name=accept