def sub_add

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

import Base

172def sub_add(+a: Nat, +b: Nat) -> {a == Nat.sub(Nat.add(a, b), b) : Nat}:
173  match b:
174    case 0n:
175      sub_add_zero(a)
176    case 1n+q:
177      %add_succ(a, q) : {a == Nat.sub(_, 1n+q) : Nat}
178      sub_add(a, q)