law mod_tail

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/conformance.bend:640

import Base

640law mod_tail:
641  for +x: Nat
642  for +k: Nat
643  {Nat.mod(Nat.add(x, mul64(k)), 64n) == Nat.mod(x, 64n) : Nat}