Alexandre Soares (Nov 05 2024 at 22:56): Alexandre Soares (Nov 05 2024 at 22:56):I'm working in Complex_Main and I'm trying to prove
lemma
fixes ε :: real
assumes "ε > 0" and "36 * (9 + ε) < (18 + ε)^2"
shows "6 * sqrt (9 + ε) < 18 + ε"
Should be simple, but nothing I've tried works, not even Sledgehammer can find a proof. Any pointers?
Christian Pardillo Laursen (Nov 06 2024 at 12:49):lemma
fixes ε :: real
assumes "ε > 0" and "36 * (9 + ε) < (18 + ε)^2"
shows "6 * sqrt (9 + ε) < 18 + ε"
apply (rule power2_less_imp_less)
using assms apply simp_all
done
find_theorems is your friend - I found that theorem by typing find_theorems intro power2
Alexandre Soares (Nov 06 2024 at 14:45):Didn't know about find_theorems, thank you!
Christian Pardillo Laursen (Nov 06 2024 at 15:44):It's indispensable for working in bigger theories, I use it all the time. This tutorial is quite useful https://isabelle.systems/cookbook/src/commands/Find.thy
Yong Kiam (Nov 06 2024 at 15:46):note that if you're in Isabelle/JEdit there's a nice Query panel you can use for this
Last updated: Dec 21 2024 at 16:20 UTC