~/jendhub

def bq.lt_cancel

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

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

257def bq.lt_cancel(s: Nat, -r: Nat, -u: Nat) -> {Nat.is_lt(Nat.add(s, r), Nat.add(s, u)) == Nat.is_lt(r, u) : Bool}:
258  match s:
259    case 0n:
260      {==}
261    case 1n+p:
262      bq.lt_cancel(p, r, u)

Uses (4)

Used by (1)