law pos_add

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:233

import Base

233law pos_add:
234  for +n: Nat
235  for +x: Nat
236  for +y: Nat
237  {pos(n, Nat.add(x, y)) == Nat.add(pos(n, x), pos(n, y)) : Nat}