Possible mistake in `la_generic` definition
In the specification for the la_generic rule, when describing how to sum the processed inequalities, the spec says this:
The operator ⋈ is ≈ if all operators are ≈, > if all are either ≈ or >, and ≥ otherwise.
This implies that, if we have one > operator and one \geq, the resulting operator should be \geq. However, I believe in this case the operator should be > (intuitively, if we have a > b and c \geq d, we can infer that a + c > b + d). I propose the correct definition should be:
The operator ⋈ is ≈ if all operators are ≈, ≥ if all are either ≈ or ≥, and > otherwise.
This mistake does not affect the correctness of the rule, since a > b \rightarrow a \geq b, but fixing it would allow more valid applications.