law add16_not_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/chacha20poly1305.bend:216

import Base

216# a + 16 is not below 16, and (a + 16) - 16 == a.
217law add16_not_lt:
218  for +a: Nat
219  {Nat.is_lt(Nat.add(a, 16n), 16n) == False{} : Bool}