equal
deleted
inserted
replaced
984 by (simp add: not_less [symmetric] mult_less_cancel_right_disj) |
984 by (simp add: not_less [symmetric] mult_less_cancel_right_disj) |
985 |
985 |
986 lemma mult_le_cancel_left: |
986 lemma mult_le_cancel_left: |
987 "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" |
987 "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" |
988 by (simp add: not_less [symmetric] mult_less_cancel_left_disj) |
988 by (simp add: not_less [symmetric] mult_less_cancel_left_disj) |
|
989 |
|
990 lemma mult_le_cancel_left_pos: |
|
991 "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b" |
|
992 by (auto simp: mult_le_cancel_left) |
|
993 |
|
994 lemma mult_le_cancel_left_neg: |
|
995 "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a" |
|
996 by (auto simp: mult_le_cancel_left) |
|
997 |
|
998 end |
|
999 |
|
1000 context ordered_ring_strict |
|
1001 begin |
|
1002 |
|
1003 lemma mult_less_cancel_left_pos: |
|
1004 "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b" |
|
1005 by (auto simp: mult_less_cancel_left) |
|
1006 |
|
1007 lemma mult_less_cancel_left_neg: |
|
1008 "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a" |
|
1009 by (auto simp: mult_less_cancel_left) |
989 |
1010 |
990 end |
1011 end |
991 |
1012 |
992 text{*Legacy - use @{text algebra_simps} *} |
1013 text{*Legacy - use @{text algebra_simps} *} |
993 lemmas ring_simps[noatp] = algebra_simps |
1014 lemmas ring_simps[noatp] = algebra_simps |