def bq.half_lt

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:350

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

350def bq.half_lt(s: Nat, h: {Nat.is_lt(0n, s) == True{} : Bool}) -> {Nat.is_lt(U.uq.half(s), s) == True{} : Bool}:
351  match s:
352    case 0n:
353      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
354    case 1n+p:
355      match p:
356        case 0n:
357          {==}
358        case 1n+ +q:
359          bq.lt_succ_le(U.uq.half(q), q, bq.half_le(q))