*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Inequality assumption*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 5 Jul 2016 17:31:17 +0200*In-reply-to*: <CAAi=getJaN5eqQidrG5tKvk9ONV-99pe0m9ODn=zNydgDrn+OA@mail.gmail.com>*References*: <CAAi=getJaN5eqQidrG5tKvk9ONV-99pe0m9ODn=zNydgDrn+OA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

Cheers, Manuel On 05/07/16 17:22, Omar Jasim 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

**References**:**[isabelle] Inequality assumption***From:*Omar Jasim

- Previous by Date: Re: [isabelle] Inequality assumption
- Next by Date: Re: [isabelle] Mean value theorem for has_vector_derivative
- Previous by Thread: Re: [isabelle] Inequality assumption
- Next by Thread: [isabelle] Isabelle Workshop Program
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list