def bq.lt_one

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

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

import Base

227def bq.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
228  match x:
229    case 0n:
230      {==}
231    case 1n+p:
232      match p:
233        case 0n:
234          Empty.absurd({1n == 0n : Nat}, bq.ft(e))
235        case 1n+q:
236          Empty.absurd({2n+q == 0n : Nat}, bq.ft(e))

Uses (5)

Used by (1)

bend-osdev-algo@0.1.0.0/PROOF:ba.run