def zsub

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/arith.bend:129

import Base

129def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}:
130  match b:
131    case 0n:
132      {==}
133    case 1n+q:
134      {==}