# Re: [isabelle] prove simple inequality

```There is actually another option since recently (assuming you are using the repository version of Isabelle). If you are interested in a step-by-step proof but don't won't to do the work yourself, you can try calling sledgehammer with the isar_proofs option:

lemma test:
assumes a1: "(a::real)>0" and a2: "a<1" and b1: "(b::real)>0" and b2: "b<1"
shows "a+b - a*b > 0"
sledgehammer [isar_proofs, isar_compress=2]

The isar_compress option lets you control the level of detail of the generated proof(s).
On my machine, sledgehammer came up with the following proof:

proof -
have "a * b < b"
by (metis a2 b1 comm_semiring_1_class.normalizing_semiring_rules(11) mult_strict_right_mono)
hence "a * b < a + b"
thus "0 < a + b - a * b"
qed

I think the resulting proof is actually quite nice and easy to follow. (Unfortunately, it doesn't always work that well.)
The proof gets even nicer after some manual post-processing (which may be done automatically in the near future):

proof -
have "a * b < b"
by (simp add: algebra_simps a2 b1)
hence "a * b < a + b"
thus "0 < a + b - a * b"
by simp
qed

Regards,
Steffen

On 05.07.2013, at 15:02, cl-isabelle-users-request at lists.cam.ac.uk wrote:

> 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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.