feat: Nat.mul_mod (#3582) Proves `Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b)` and `Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b)`, helpful for bitblasting.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.