def zsub

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/arith.bend:90

import Base

90def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}:
91  match b:
92    case 0n:
93      {==}
94    case 1n+p:
95      {==}