equal
deleted
inserted
replaced
1056 |
1056 |
1057 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)" |
1057 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)" |
1058 by simp (* solved by linordered_ring_le_cancel_factor simproc *) |
1058 by simp (* solved by linordered_ring_le_cancel_factor simproc *) |
1059 |
1059 |
1060 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)" |
1060 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)" |
1061 by (rule mult_le_cancel_left_pos) |
1061 by simp (* solved by linordered_ring_le_cancel_factor simproc *) |
1062 (* BH: Why doesn't "simp" prove this one, like it does the last one? *) |
|
1063 |
1062 |
1064 |
1063 |
1065 subsection {* Embedding numbers into the Reals *} |
1064 subsection {* Embedding numbers into the Reals *} |
1066 |
1065 |
1067 abbreviation |
1066 abbreviation |