def zero_subtract

stelliferous@0.0.2.0 · proofs/nat_order.bend:35

import Base

35def zero_subtract(value: Nat) -> {Nat.sub(0n,value) == 0n : Nat}:
36  match value:
37    case 0n: {==}
38    case 1n+rest: {==}