En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f

Demostrar con Lean4 que \(a\), \(b\), \(c\), \(d\) y \(f\) son números reales tales que \(a \leq b\) y \(c < d\), entonces \[a + e^c + f \leq b + e^d + f\] Para ello, completar la siguiente teoría de Lean4:

Demostraciones en lenguaje natural (LN)

1ª demostración en LN

Aplicando a la hipótesis 3 (\(c < d\)) la monotonía de la exponencial, se tiene \[e^c < e^d\] que, junto a la hipótesis 1 (\(a \leq b\)) y la monotonía de la suma da \[a + e^c < b + e^d\] y, de nuevo por la monotonía de la suma, se tiene \[a + e^c + f < b + e^d + f\] 2ª demostración en LN

Tenemos que demostrar que
\[(a + e^c) + f < (b + e^d) + f\] que, por la monotonía de la suma, se reduce a las siguientes dos desigualdades: \begin{align} &a + e^c < b + e^d \tag{1} \\ &f \leq f \tag{2} \end{align} La (1), de nuevo por la monotonía de la suma, se reduce a las siguientes dos: \begin{align} &a \leq b \tag{1.1} \\ &e^c < e^d \tag{1.2} \end{align}