feat: `IntX` modulo lemmas (#7704) This PR adds lemmas about the modulo operation defined on signed bounded integers. The results depend on the lemma ```lean theorem BitVec.toInt_srem (a b : BitVec w) : (a.srem b).toInt = a.toInt.tmod b.toInt := sorry ``` which is missing at the time of posting the PR.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).