law mod_mul_mod_r

lawful-words@0.1.0.0 · proof_nat.bend:1261

import Base

1261law mod_mul_mod_r:
1262  for +y: Nat
1263  for +u: Nat
1264  for +m: Nat
1265  {Nat.mod(Nat.mul(y, Nat.mod(u, m)), m) == Nat.mod(Nat.mul(y, u), m) : Nat}