law mod_mod_mul

lawful-words@0.1.0.0 · proof_nat.bend:1282

import Base

1282# (a % (x * y)) % x = a % x.
1283law mod_mod_mul:
1284  for +a: Nat
1285  for +x: Nat
1286  for +y: Nat
1287  {Nat.mod(Nat.mod(a, Nat.mul(x, y)), x) == Nat.mod(a, x) : Nat}