~/jendhub

def bq.sub_le0

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

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

307def bq.sub_le0(h: Nat, l: Nat, e: {Nat.is_le(h, l) == True{} : Bool}) -> {Nat.sub(h, l) == 0n : Nat}:
308  match h l:
309    case 0n _:
310      {==}
311    case 1n+hp 0n:
312      Empty.absurd({1n+hp == 0n : Nat}, bq.ft(e))
313    case 1n+hp 1n+lp:
314      bq.sub_le0(hp, lp, e)

Uses (6)

Used by (1)