def un.sub_add

bend-osdev-u32@0.1.0.0 · PROOF.bend:101

import Base

101def un.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
102  %un.add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
103  un.sub_add_l(y, r)