def zsub
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as Arithimport Base
129def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}:
130 match b:
131 case 0n:
132 {==}
133 case 1n+q:
134 {==}
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as Arithimport Base
129def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}:
130 match b:
131 case 0n:
132 {==}
133 case 1n+q:
134 {==}