Poly.step_alg: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/poly.bend as Poly
Lines 25-32 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/poly.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/poly.bend&start_line=25&end_line=32

import Base

# (r (a + n)) X == a (r X) + n (r X)
law step_alg:
  for +r: Nat
  for +a: Nat
  for +n: Nat
  for +x: Nat
  for +p: Nat
  {Nat.add(Nat.mul(Nat.mul(r, Nat.add(a, n)), x), p) == Nat.add(Nat.mul(a, Nat.mul(r, x)), Nat.add(Nat.mul(n, Nat.mul(r, x)), p)) : Nat}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=Nat.mul
  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=mul_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm