Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] prove simple inequality

Email Gateway (Aug 19 2022 at 11:26):

From: Michael Vu <michael.vu@rwth-aachen.de>
Dear Isabelle experts,

i have following simple lemma:

lemma ineq:
"(a::real) > 0 ⟹ a < 1 ⟹ (b::real) > 0 ⟹ b < 1 ⟹ (a + b - a * b) > 0"

My problem is that i cannot prove this lemma, i tried tools like 'simp' with algebra/field_simps etc. but i cannot figure out
which rule to use. Any help would be appreciated!

Regards,
Michael

Last updated: Nov 21 2024 at 12:39 UTC