def wn.sub_add

bend-osdev-word64@0.1.1.0 · proof_value.bend:89

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

89def wn.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
90  %UL.nat_add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
91  wn.sub_add_l(y, r)