Negate.sub_mod: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as Negate
Lines 173-180 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&start_line=173&end_line=180

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
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

# a + (m - b) = (a + m) - b, for b < m
def sub_mod(+mp: Nat, +a: Nat, +b: Nat, +nb: Nat, +hlt: {Nat.is_lt(b, 1n+mp) == True{} : Bool}, +hn: {Nat.add(nb, b) == 1n+mp : Nat}) -> {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), Nat.mod(b, 1n+mp)), 1n+mp) : Nat}:
  %Equal.sym(Nat, Nat.mod(b, 1n+mp), b, NR.mod_of(0n, mp, b, hlt)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), _), 1n+mp) : Nat}
  %Equal.sym(Nat, 1n+mp, Nat.add(nb, b), Equal.sym(Nat, Nat.add(nb, b), 1n+mp, hn)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, _), b), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.add(a, Nat.add(nb, b)), Nat.add(Nat.add(a, nb), b), Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(a, Nat.add(nb, b)), NA.add_assoc(a, nb, b))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(b, Nat.add(a, nb)), NA.add_comm(Nat.add(a, nb), b)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.sub(Nat.add(b, Nat.add(a, nb)), b), Nat.add(a, nb), N.add_sub_cancel(b, Nat.add(a, nb))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}
  {==}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_sub_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_of