Re: [isabelle] Inequality assumption

HOL is a total logic, so all functions must be defined for all inputs of the corresponding type. In Isabelle/HOL, division by zero is therefore defined to yield zero, and with that, the lemma you cited holds.

Understanding the definitions of the constants involved in a statement and how they differ from âstandardâ mathematical definitions is crucial.



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


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