This PR implements model construction for offset constraints in the `grind` tactic.
Int.tdiv
Int.tmod
Simp.Config.implicitDefEqProofs
Lean.loadPlugin