def sub_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:90

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

90def sub_cancel(+c: Nat, +m: Nat, +r: Nat) -> {Nat.sub(Nat.add(c, Nat.add(m, r)), m) == Nat.add(c, r) : Nat}:
91  %Equal.sym(Nat, Nat.add(c, Nat.add(m, r)), Nat.add(m, Nat.add(c, r)), NA.add_swap(c, m, r)) : {Nat.sub(_, m) == Nat.add(c, r) : Nat}
92  N.add_sub_cancel(m, Nat.add(c, r))