Fieldpow.arr4: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as Fieldpow
Lines 291-296 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&start_line=291&end_line=296

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

def arr4(+m: Nat, +d: Nat, +o: Nat) -> {Nat.add(m, Nat.add(Nat.add(d, o), o)) == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}:
  %Equal.sym(Nat, Nat.add(Nat.add(d, o), o), Nat.add(d, Nat.add(o, o)), NA.add_assoc(d, o, o)) : {Nat.add(m, _) == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}
  %Equal.sym(Nat, Nat.add(m, Nat.add(d, Nat.add(o, o))), Nat.add(d, Nat.add(m, Nat.add(o, o))), NA.add_swap(m, d, Nat.add(o, o))) : {_ == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(d, o), Nat.add(m, o)), Nat.add(d, Nat.add(o, Nat.add(m, o))), NA.add_assoc(d, o, Nat.add(m, o))) : {Nat.add(d, Nat.add(m, Nat.add(o, o))) == _ : Nat}
  %Equal.sym(Nat, Nat.add(o, Nat.add(m, o)), Nat.add(m, Nat.add(o, o)), NA.add_swap(o, m, o)) : {Nat.add(d, Nat.add(m, Nat.add(o, o))) == Nat.add(d, _) : Nat}
  {==}

Uses (5):
  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/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