law add16_sub
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend as Chacha20poly1305import Base
225law add16_sub:
226 for +a: Nat
227 {Nat.sub(Nat.add(a, 16n), 16n) == a : Nat}
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend as Chacha20poly1305import Base
225law add16_sub:
226 for +a: Nat
227 {Nat.sub(Nat.add(a, 16n), 16n) == a : Nat}