def bq.sub_zero

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

import Base

273def bq.sub_zero(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
274  match x:
275    case 0n:
276      {==}
277    case 1n+p:
278      {==}