Refactor LTV check

[QGarchery]

This refactor should be functionally equivalent to the previous one, which is verified here.

Motivation to do this refactor:

• it makes it clearer why the computation ltv - PRE_LLTV won't revert
• it makes the computation more efficient
• we can document and verify that it is functionally the same as before

[peyha]

LGTM, it removes an useless variable

[MathisGD]

This refactor should be functionally equivalent to the previous one, which is verified here.

This isn't super intuitive. Why the rounding doesn't cause issues?

Please wait for my approval before merging

[QGarchery]

This isn't super intuitive. Why the rounding doesn't cause issues?

I agree that it isn't intuitive, that's why I wanted to verify it in Certora.

Here is the proof that $$\lceil \frac{a b}{c} \rceil > d \Leftrightarrow a > \lfloor \frac{cd}{b} \rfloor$$. Then we get the result with $$a := borrowed$$, $$b := 1e18$$, $$c = collateralQuoted$$ and $$d = preLltv$$. We have :

1. $$\lceil \frac{a b}{c} \rceil > d \Leftrightarrow \frac{a b}{c} > d$$
2. $$\frac{a b}{c} > d \Leftrightarrow a > \frac{cd}{b}$$
3. $$a > \frac{cd}{b} \Leftrightarrow a > \lfloor \frac{cd}{b} \rfloor$$

2 is obvious, 1&3 are similar result, so let's just show 1. Because $$\lceil x \rceil$$ is an increasing function, we only have to show: $$\lceil \frac{a b}{c} \rceil > d \Rightarrow \frac{a b}{c} > d$$. By contraposition: if $$\frac{ab}{c} \leq d$$, then by definition of $$\lceil x \rceil$$ and because $$d$$ is an integer we also have $$\lceil \frac{a b}{c} \rceil \leq d$$.