law mod_quotient

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

import Base

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