[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!

Regards,
Michael




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