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.