Arith.mod_mul_r: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as Arith
Lines 150-160 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&start_line=150&end_line=160

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

# (x (y mod n)) mod n == (x y) mod n   (Mathlib Nat.mul_mod)
def mod_mul_r(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.mul(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.mul(x, y), 1n+bp) : Nat}:
  +n = {1n+bp : Nat}
  +qy = Nat.div(y, n)
  +my = Nat.mod(y, n)
  +e = Equal.trans(Nat, Nat.mul(x, y), Nat.mul(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)),
    Equal.cong(Nat, Nat, z => Nat.mul(x, z), y, Nat.add(Nat.mul(qy, n), my), dm_eq(bp, y)),
    Equal.trans(Nat, Nat.mul(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(x, Nat.mul(qy, n)), Nat.mul(x, my)), Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)),
      A.mul_add_left(x, Nat.mul(qy, n), my),
      Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(x, my)), Nat.mul(x, Nat.mul(qy, n)), Nat.mul(Nat.mul(x, qy), n), Equal.sym(Nat, Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, Nat.mul(qy, n)), A.mul_assoc(x, qy, n)))))
  Equal.sym(Nat, Nat.mod(Nat.mul(x, y), n), Nat.mod(Nat.mul(x, my), n), Equal.trans(Nat, Nat.mod(Nat.mul(x, y), n), Nat.mod(Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)), n), Nat.mod(Nat.mul(x, my), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.mul(x, y), Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)), e), absorb(bp, Nat.mul(x, qy), Nat.mul(x, my))))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=absorb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq