Re: [isabelle] Natural property



On Fri, 22 Sep 2006, Gabriele Pozzani wrote:

> Now from
> a * 1 < b * (a + 1)
> I would demonstrate the thesis but I don't know how to do that.

You just need to use the Ex-Introduction rule, i.e. append

thus ?thesis  
  apply(rule_tac x="1" in exI) apply (rule_tac x="a+1" in exI)
    by simp

to your proof.

Amine.





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