RFC: disjunction of guard conditions for grind_pattern

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 <|>.

Start by reading the existing grind_pattern handling of side-condition lists and the motivating example in pull request 11584. Define how the proposed <|> disjunction combines with guard conditions, while preserving the current conjunction behavior, and verify the mod_eq_of_lt example demonstrates the intended result.