~/jendhub

def bq.sub0_le

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

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

316def bq.sub0_le(h: Nat, l: Nat, e: {Nat.sub(h, l) == 0n : Nat}) -> {Nat.is_le(h, l) == True{} : Bool}:
317  match h l:
318    case 0n 0n:
319      {==}
320    case 0n 1n+lp:
321      {==}
322    case 1n+hp 0n:
323      Empty.absurd({Nat.is_le(1n+hp, 0n) == True{} : Bool}, bq.sz(hp, e))
324    case 1n+hp 1n+lp:
325      bq.sub0_le(hp, lp, e)

Uses (6)

Used by (1)