law mod_tail

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

import Base

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