ProofFastFind.gtop.go: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_find.bend as ProofFastFind
Lines 401-408 of lawful-bytes@0.1.1.0/proof_fast_find.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&start_line=401&end_line=408

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N
import lawful-arrays@0.1.0.0/proof_base.bend as AB

def gtop.go(+tt: Nat, +m: Nat, +ht: {Nat.is_lt(tt, m) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(Nat.sub(m, 1n), 0n), tt) == False{} : Bool}:
  match m:
    case 0n:
      Empty.absurd({Nat.is_lt(0n, tt) == False{} : Bool}, AB.lt_zero_absurd(tt, ht))
    case 1n+p:
      %Equal.sym(Nat, Nat.sub(Nat.sub(p, 0n), 0n), Nat.sub(p, 0n), N.sub_zero(Nat.sub(p, 0n))) : {Nat.is_lt(_, tt) == False{} : Bool}
      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(_, tt) == False{} : Bool}
      N.le_not_lt(tt, p, Equal.trans(Bool, Nat.is_le(tt, p), Nat.is_lt(tt, 1n+p), True{}, Equal.sym(Bool, Nat.is_lt(tt, 1n+p), Nat.is_le(tt, p), N.lt_succ_iff(tt, p)), ht))

Uses (12):
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_zero_absurd
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_not_lt
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_succ_iff
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=sub_zero