# Re: [isabelle] prove simple inequality

```This is a cute one. For a start, it is (a) non-linear and (b) not provable by
just multiplying things out and reasoning modulo AC, which is essentially what
algebra/field_simps are doing.

At first I tried what I thought to be the perfect match, namely I imported
"~~/src/HOL/Library/Sum_of_Squares", a proof procedure esp for non-linear
inequalities by John Harrison. Unfortunately, although the problem is simple,
"by sos" did not work (in the amount of time I waited). Then I did what Manuel

comm_monoid_mult_class.mult.left_neutral

Not very informative, but it does the job. Although sledgehammer is unlikely to
be effective on more complicated arithmetic formulas.

Having seen Manuel's proof and the fact that one assumption is not needed, I
tried John's sos again and got this proof with certificate:

by (sos_cert "((((A<0 * (A<1 * A<2)) * R<1) + (((A<2 * R<1) * (R<1/4 * [a]^2)) +
(((A<1 * R<1) * (R<1/4 * [~1*a + b]^2)) + (((A<0 * R<1) * (R<1/4 * [a]^2)) +
(((A<=0 * (A<2 * R<1)) * (R<1/4 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/4 *
[1]^2))))))))")

Again, a bit cryptic, but for general non-linear inequalities sos is the
recommended method.

Tobias

Am 04/07/2013 11:48, schrieb Michael Vu:
> 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.