Re: [isabelle] Inequality assumption



Dear Omar,

In Isabelle/HOL, we are having a definition that x/0=0:

assumes inverse_zero [simp]: "inverse 0 = 0"

in this case, divide_right_mono holds as a/0 = b/0 = 0, but whether this makes sense to mathematician is another question...

Best,
Wenda

On 2016-07-05 16: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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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