law mod_quotient

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

import Base

613# The quotient accumulator never affects the remainder computed by divmod.
614law mod_quotient:
615  for +x: Nat
616  for +m: Nat
617  for +d: Nat
618  for +e: Nat
619  for +r: Nat
620  {Pair.snd(Nat, Nat, Nat.divmod.go(x, m, d, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(x, m, e, r)) : Nat}