RFC: disjunction of guard conditions for grind_pattern

[pirapira]

I propose extending grind_pattern so that it can take conjunctive normal form (conjunction of disjunctions) of side-conditions. Currently grind_pattern can take a list of side-conditions. The list is interpreted as a conjunction.

The motivating example for the change was mod_eq_of_lt: a < b -> a % b = a. It's desirable to guard against using this lemma on completely concrete examples like 2 % 1024. However, both 2 % b and a % 1024 can benefit from the lemma. [edit: but I realized that the a % 1024 case is already solvable by lia]

To distinguish the wanted case and unwanted case, the precise guard would look like

grind_pattern mod_eq_of_lt => a % b where
  not_value a <|> not_value b
  guard a < b

with disjunction <|>.

[pirapira]

I used Sonnet-4.5 to implement this in #11791 .