# 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.*