~/jendhub

def bq.lt_succ_le

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

import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch
import Base

238def bq.lt_succ_le(x: Nat, y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_lt(x, 1n+y) == True{} : Bool}:
239  match x y:
240    case 0n _:
241      {==}
242    case 1n+xp 0n:
243      Empty.absurd({Nat.is_lt(1n+xp, 1n) == True{} : Bool}, bq.ft(h))
244    case 1n+xp 1n+yp:
245      bq.lt_succ_le(xp, yp, h)

Uses (6)

Used by (1)