def bq.sub_pos

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

import Base

296def bq.sub_pos(l: Nat, h: Nat, e: {Nat.is_lt(l, h) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(h, l)) == True{} : Bool}:
297  match l h:
298    case 0n 0n:
299      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(e))
300    case 0n 1n+hp:
301      {==}
302    case 1n+lp 0n:
303      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(e))
304    case 1n+lp 1n+hp:
305      bq.sub_pos(lp, hp, e)