Negate.combine: 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 65-82 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=65&end_line=82

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

# (l + h B) + (h' B + l') = (l' + l) + (h' + h) B
def combine(+l: Nat, +h: Nat, +h2: Nat, +l2: Nat, +b: Nat) -> {Nat.add(Nat.add(l, Nat.mul(h, b)), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}:
  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.add(l, _), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
  %Equal.sym(Nat, Nat.add(l, Nat.mul(b, h)), Nat.add(Nat.mul(b, h), l), NA.add_comm(l, Nat.mul(b, h))) : {Nat.add(_, Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(_, l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_assoc(Nat.mul(b, h), l, Nat.add(Nat.mul(b, h2), l2))) : {_ == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), _) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
  %Equal.sym(Nat, Nat.add(l2, l), Nat.add(l, l2), NA.add_comm(l2, l)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(_, Nat.mul(Nat.add(h2, h), b)) : Nat}
  %Equal.sym(Nat, Nat.add(h2, h), Nat.add(h, h2), NA.add_comm(h2, h)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.mul(_, b)) : Nat}
  %Equal.sym(Nat, Nat.mul(Nat.add(h, h2), b), Nat.add(Nat.mul(h, b), Nat.mul(h2, b)), NA.mul_add_right(h, h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), _) : Nat}
  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(_, Nat.mul(h2, b))) : Nat}
  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), _)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(l, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))), NA.add_assoc(l, l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}
  %Equal.sym(Nat, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(Nat.mul(b, h), Nat.add(l2, Nat.mul(b, h2))), NA.add_swap(l2, Nat.mul(b, h), Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, _) : Nat}
  %Equal.sym(Nat, Nat.add(l2, Nat.mul(b, h2)), Nat.add(Nat.mul(b, h2), l2), NA.add_comm(l2, Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, Nat.add(Nat.mul(b, h), _)) : Nat}
  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_swap(l, Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}
  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.mul(b, h), _) : Nat}
  {==}

Uses (9):
  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.mul
  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/lemmas/proofs/nat_algebra.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm