def pw

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as Eqf

import Base

18def pw(+pp: Nat, +A: Nat, +B: Nat) -> Nat:
19  Nat.sub(Nat.add(A, 1n+pp), B)

Uses (3)