RFC: adding `grind_pattern` for `Int.zero_[tdiv, tmod, fmod]` and `Int.[tdiv, tmod, fmod]_zero` lemmas

This RFC is the result of a conversation held during ItaLean.

I propose adding grind patterns for some lemmas around tdiv/tmod and fdiv/fmod.
A starting set would be:

• zero_fmod, fmod_zero (used in BitVec.toInt_smod)
• zero_tdiv, tdiv_zero (used in BitVec.toInt_sdiv)
• zero_tmod, tmod_zero (used in BitVec.toInt_srem)

Moreover, to make sure that grind can really benefit from these theorem in BitVec lemmas, I realized we probably also want:

• BitVec.[toInt_smod, toInt_sdiv, toInt_srem] - I've seen that some BitVec.toInt_* lemmas are already grind-tagged, adding these lemmas seems to me consistent with what's currently happening in BitVec
• Int.bmod_eq_of_le, to take care of the moduli resulting from the toInt_* conversions - afaiu, for the lemmas I am referring to, this is typically satisfied trivially

Some simple lemmas that become grindable with this strategy:

attribute [grind? =] Int.tdiv_zero
attribute [grind? =] Int.fmod_zero
attribute [grind? =] Int.tmod_zero
attribute [grind? =] BitVec.toInt_sdiv
attribute [grind? =] BitVec.toInt_srem
attribute [grind? =] BitVec.toInt_smod
attribute [grind? =] Int.bmod_eq_of_le

example {x : BitVec 32} :  (x.sdiv 0#32).toInt = 0 := by grind

example {x : BitVec 32} :  (x.smod 0#32).toInt = x.toInt := by grind

example {x : BitVec 32} :  (x.srem 0#32).toInt = x.toInt := by grind

Having these lemmas in grind, would allow us to reason about bitvectors as integers, complementing bv_decide's functionalities when we have toInt conversions.

The alternative would be tagging for grind the BitVec.[smod, srem, sdiv]_zero and BitVec.zero_[smod, srem, sdiv] lemmas directly. However, that would probably require thinking more carefully about a BitVec strategy for grind (also, afaiu, no theorem of this form is currently tagged grind in BitVec).

Start by reviewing the proposed Int.tdiv_zero, Int.tmod_zero, Int.fmod_zero, Int.bmod_eq_of_le, and BitVec.toInt_sdiv/toInt_srem/toInt_smod grind attributes, along with the linked BitVec lemmas. Compare this approach with tagging the BitVec zero and division/modulo lemmas directly. Done means agreeing on a grind strategy and validating the three example goals with the selected attributes.