def pm

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as Step

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

22def pm(+one: Nat) -> Nat:
23  Nat.sub(C.shift(130n, one), 5n)

Uses (3)