def uq.sub_add

bend-osdev-algo@0.1.0.0 · proof_u32.bend:103

import Base

103def uq.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
104  %uq.add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
105  uq.sub_add_l(y, r)