Negate.neg_v: 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 161-168 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=161&end_line=168

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

# neg_raw(c, b) + b = m, for b < m = 2^256 - c
def neg_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:
  +nb = LV.ev(L.neg_raw(c, b))
  +bv = LV.ev(b)
  +cv = LV.ev(c)
  +hbc = I.lt_subst_r(Nat.add(bv, cv), Nat.add(1n+mp, cv), C.shift(256n, one), hm, N.lt_add_r2(bv, 1n+mp, cv, hb))
  +e1 = Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(nb, Nat.add(bv, cv)), Nat.add(1n+mp, cv), NA.add_assoc(nb, bv, cv), Equal.trans(Nat, Nat.add(nb, Nat.add(bv, cv)), C.shift(256n, one), Nat.add(1n+mp, cv), neg_t(one, h1, c, b, hbc), Equal.sym(Nat, Nat.add(1n+mp, cv), C.shift(256n, one), hm)))
  NR.add_cancel(cv, Nat.add(nb, bv), 1n+mp, Equal.trans(Nat, Nat.add(cv, Nat.add(nb, bv)), Nat.add(Nat.add(nb, bv), cv), Nat.add(cv, 1n+mp), NA.add_comm(cv, Nat.add(nb, bv)), Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(1n+mp, cv), Nat.add(cv, 1n+mp), e1, NA.add_comm(1n+mp, cv))))

Uses (16):
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=neg_t
  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=lt_add_r2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=neg_raw