def arr4

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

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

291def 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}:
292  %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}
293  %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}
294  %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}
295  %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}
296  {==}