def arr3

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldpow.bend:284

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

284def arr3(+d: Nat, +o: Nat, +h: Nat) -> {Nat.add(Nat.add(d, o), h) == Nat.add(Nat.add(h, d), o) : Nat}:
285  %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}
286  %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}
287  %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}
288  %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}
289  {==}