[isabelle] prove simple inequality

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!


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