Omar Jasim

2016-07-05 15:25:36 UTC

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

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