def bq.half_le

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

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

339def bq.half_le(q: Nat) -> {Nat.is_le(U.uq.half(q), q) == True{} : Bool}:
340  match q:
341    case 0n:
342      {==}
343    case 1n+p:
344      match p:
345        case 0n:
346          {==}
347        case 1n+ +r:
348          bq.le_succ_r(U.uq.half(r), r, bq.half_le(r))