~/jendhub

def bq.le_succ_r

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

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

161def bq.le_succ_r(x: Nat, y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x, 1n+y) == True{} : Bool}:
162  match x y:
163    case 0n _:
164      {==}
165    case 1n+xp 0n:
166      Empty.absurd({Nat.is_le(1n+xp, 1n) == True{} : Bool}, bq.ft(h))
167    case 1n+xp 1n+yp:
168      bq.le_succ_r(xp, yp, h)

Uses (5)

Used by (1)