Exercise 4.1 solved

[GabrielJP314]

Proving that $\left(a < (a+b)\;/\;2 \;\land\; (a+b)\;/\;2 < b\right)\leftrightarrow\;a + 1 < b$ for integers $a$ and $b$, and that $\left\lceil \log_2(n + 1) \right\rceil \le h$ for integer $h$ and $n < 2^h$.

[GabrielJP314]

Now it's correct!

[arademaker]

Hi @GabrielJP314, take a look at my commit message here. First, your rcase was doing a case analysis; the exercise explicitly said not to do it. Second, the theorems were supposed to use the rule of floors/rule of ceilings. They are already in Mathlib as Int.le_floor and Int.ceil_le, so both proofs
now appeal to them directly instead of reasoning around them.