equal
deleted
inserted
replaced
1133 by (simp add: not_less [symmetric] mult_less_cancel_right_disj) |
1133 by (simp add: not_less [symmetric] mult_less_cancel_right_disj) |
1134 |
1134 |
1135 lemma mult_le_cancel_left: |
1135 lemma mult_le_cancel_left: |
1136 "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" |
1136 "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" |
1137 by (simp add: not_less [symmetric] mult_less_cancel_left_disj) |
1137 by (simp add: not_less [symmetric] mult_less_cancel_left_disj) |
|
1138 |
|
1139 lemma mult_le_cancel_left_pos: |
|
1140 "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b" |
|
1141 by (auto simp: mult_le_cancel_left) |
|
1142 |
|
1143 lemma mult_le_cancel_left_neg: |
|
1144 "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a" |
|
1145 by (auto simp: mult_le_cancel_left) |
|
1146 |
|
1147 end |
|
1148 |
|
1149 context ordered_ring_strict |
|
1150 begin |
|
1151 |
|
1152 lemma mult_less_cancel_left_pos: |
|
1153 "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b" |
|
1154 by (auto simp: mult_less_cancel_left) |
|
1155 |
|
1156 lemma mult_less_cancel_left_neg: |
|
1157 "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a" |
|
1158 by (auto simp: mult_less_cancel_left) |
1138 |
1159 |
1139 end |
1160 end |
1140 |
1161 |
1141 text{*Legacy - use @{text algebra_simps} *} |
1162 text{*Legacy - use @{text algebra_simps} *} |
1142 lemmas ring_simps[noatp] = algebra_simps |
1163 lemmas ring_simps[noatp] = algebra_simps |