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.
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and