ProofBsearch.bq.half_lt_pw: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch
Lines 361-383 of bend-osdev-algo@0.1.0.0/proof_bsearch.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&start_line=361&end_line=383

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U

# s < 2p: s / 2 < p
def bq.half_lt_pw(s: Nat, p: Nat, h: {Nat.is_lt(s, Nat.double(p)) == True{} : Bool}) -> {Nat.is_lt(U.uq.half(s), p) == True{} : Bool}:
  match s:
    case 0n:
      match p:
        case 0n:
          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
        case 1n+pp:
          {==}
    case 1n+sp:
      match sp:
        case 0n:
          match p:
            case 0n:
              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
            case 1n+pp:
              {==}
        case 1n+q:
          match p:
            case 0n:
              Empty.absurd({Nat.is_lt(1n+U.uq.half(q), 0n) == True{} : Bool}, bq.ft(h))
            case 1n+pp:
              bq.half_lt_pw(q, pp, h)

Uses (7):
  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=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_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.half