Suppose I have two formulas (consisting in one or more inequations) : $$\left\{\begin{array}{l}A \le B + 1\\ C \le B\end{array}\right., \quad A \le C$$
Now, I want to simplify the first formula because by transitivity I find $$\left\{\begin{array}{l}A \le B\\ C \le B\end{array}\right.$$ Which is a better system because more precise.
My problem is that I know I can't solve it (I don't want to, actually), I just want to simplify this kind of system and I can't find a simple method to do it.
Another problem comes when I have this kind of system :
\begin{equation}\left\{\begin{array}{l}A \le B + 1\\ C \le D\end{array}\right., \quad A \le C\end{equation}
In this case, we have $$A \le B + 1 \land A \le D \implies A \le \text{min}(B + 1, D)$$ and even though this is precise, it's not the kind of thing I want because it adds complexity.