Fieldpow.arr3: 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 284-289 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=284&end_line=289

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

def arr3(+d: Nat, +o: Nat, +h: Nat) -> {Nat.add(Nat.add(d, o), h) == Nat.add(Nat.add(h, d), o) : Nat}:
  %Equal.sym(Nat, Nat.add(Nat.add(d, o), h), Nat.add(d, Nat.add(o, h)), NA.add_assoc(d, o, h)) : {_ == Nat.add(Nat.add(h, d), o) : Nat}
  %Equal.sym(Nat, Nat.add(o, h), Nat.add(h, o), NA.add_comm(o, h)) : {Nat.add(d, _) == Nat.add(Nat.add(h, d), o) : Nat}
  %Equal.sym(Nat, Nat.add(h, d), Nat.add(d, h), NA.add_comm(h, d)) : {Nat.add(d, Nat.add(h, o)) == Nat.add(_, o) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(d, h), o), Nat.add(d, Nat.add(h, o)), NA.add_assoc(d, h, o)) : {Nat.add(d, Nat.add(h, o)) == _ : 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_comm