~/jendhub

def bq.sub_cancel

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

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

289def bq.sub_cancel(l: Nat, -s: Nat, -t: Nat) -> {Nat.sub(Nat.add(l, s), Nat.add(l, t)) == Nat.sub(s, t) : Nat}:
290  match l:
291    case 0n:
292      {==}
293    case 1n+p:
294      bq.sub_cancel(p, s, t)

Uses (3)

Used by (1)