Rconst.sc: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as Rconst
Lines 74-79 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&start_line=74&end_line=79

import Base
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/crypto/secp256k1/semiring.bend as SR

def sc(+b: Nat, +c: Nat) -> {1n+Nat.add(b, c) == Nat.add(c, 1n+b) : Nat}:
  %Equal.sym(Nat, 1n+Nat.add(b, c), Nat.add(Nat.add(b, c), 1n), SR.succ_add(1n, Nat.add(b, c))) : {_ == Nat.add(c, 1n+b) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(b, c), 1n), Nat.add(b, Nat.add(c, 1n)), NA.add_assoc(b, c, 1n)) : {_ == Nat.add(c, 1n+b) : Nat}
  %Equal.sym(Nat, 1n+b, Nat.add(b, 1n), SR.succ_add(1n, b)) : {Nat.add(b, Nat.add(c, 1n)) == Nat.add(c, _) : Nat}
  %Equal.sym(Nat, Nat.add(c, Nat.add(b, 1n)), Nat.add(b, Nat.add(c, 1n)), NA.add_swap(c, b, 1n)) : {Nat.add(b, Nat.add(c, 1n)) == _ : Nat}
  {==}

Uses (6):
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=succ_add
  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_swap