En ℝ, si 1 < a, entonces a < aa
Demostrar con Lean4 que en \(ℝ\), si \(1 < a\), entonces \(a < aa\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a : ℝ} example (h : 1 < a) : a < a * a := by sorry |