Note: the rules in this file are not a homomorphism. Nat and Int are not homomorphism source types (they are not registered in getHomoSourceTypes): grind has builtin support for both in its cutsat solver, including the Nat to Int cast bridge, so there is no injection out of Nat or Int and none should be added. The rules here support the source types (BitVec, Fin, the fixed-width integer types), applied to the Nat and Int images their injections produce: shifts are normalized to arithmetic, testBit decomposes bitwise operations, and the %-cleanup rules remove the redundant modular wrappers introduced by the injections.

theorem Lean.Grind.Int.emod_mul_emod (m n k : Int) : m % n * k % n = m * k % n

theorem Lean.Grind.Int.mul_emod_emod (m n k : Int) : m * (n % k) % k = m * n % k