[isabelle] Inequality assumption



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



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