law mod_mul_mod_l

lawful-words@0.1.0.0 · proof_nat.bend:1242

import Base

1242law mod_mul_mod_l:
1243  for +u: Nat
1244  for +y: Nat
1245  for +m: Nat
1246  {Nat.mod(Nat.mul(Nat.mod(u, m), y), m) == Nat.mod(Nat.mul(u, y), m) : Nat}