def subtract_zero

stelliferous@0.0.2.0 · proofs/nat_order.bend:30

import Base

30def subtract_zero(+value: Nat) -> {Nat.sub(value,0n) == value : Nat}:
31  match value:
32    case 0n: {==}
33    case 1n+rest: {==}