# Re: [isabelle] prove simple inequality

Hallo,
try sledgehammer on these things. You can also use a more detailed Isar
proof:
lemma ineq:
fixes a::real and b::real
assumes "a > 0" "a < 1" "b > 0" "b < 0"
shows "a + b - a * b > 0"
proof-
from `a < 1` and `b > 0` have "b * (1 - a) > 0"
by (simp add: algebra_simps)
with `a > 0` show ?thesis
by (simp add: algebra_simps)
qed
Cheers,
Manuel
On 04/07/13 11:48, Michael Vu 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.*