Conformance.mod_quotient: law of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
Lines 613-620 of bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&start_line=613&end_line=620

import Base

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

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd