*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] prove simple inequality*From*: Michael Vu <michael.vu at rwth-aachen.de>*Date*: Thu, 04 Jul 2013 11:48:43 +0200*Priority*: normal

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

**Follow-Ups**:**Re: [isabelle] prove simple inequality***From:*Manuel Eberl

**Re: [isabelle] prove simple inequality***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Date: [isabelle] Tutorial 'Mechanised Reasoning in Economics' (Koblenz, Germany, 17 Sept.): early registration until 15 July
- Previous by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Thread: Re: [isabelle] prove simple inequality
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list