Re: [isabelle] Inequality assumption



We have taken the liberty of extending division with x/0 = 0 precisely so that a great many theorems, including the one you mention, can be proved more generally.

Larry Paulson


> On 5 Jul 2016, at 16:22, Omar Jasim <oajasim1 at sheffield.ac.uk> wrote:
> 
> Dear list,
> 
> I've seen this lemma in Fields theory:
> 
> lemma divide_right_mono:
>     "[|a â b; 0 â c|] ==> a/c â b/c"
> by (force simp add: divide_strict_right_mono le_less)
> 
> here 0 â c which I think it should be 0 < c as the division cann't done for
> zero.
> 
> Regards
> Omar





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