def sub_add_zero

bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:164

import Base

164def sub_add_zero(a: Nat) -> {a == Nat.sub(Nat.add(a, 0n), 0n) : Nat}:
165  match a:
166    case 0n:
167      {==}
168    case 1n+p:
169      %add_zero(p) : {1n+_ == 1n+Nat.add(p, 0n) : Nat}
170      {==}