equal
deleted
inserted
replaced
1143 hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero) |
1143 hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero) |
1144 assume "\<bar>b\<bar> < d" |
1144 assume "\<bar>b\<bar> < d" |
1145 thus ?thesis by (simp add: ac cpos mult_strict_mono) |
1145 thus ?thesis by (simp add: ac cpos mult_strict_mono) |
1146 qed |
1146 qed |
1147 |
1147 |
1148 lemma less_minus_self_iff: |
|
1149 "a < - a \<longleftrightarrow> a < 0" |
|
1150 by (simp only: less_le less_eq_neg_nonpos equal_neg_zero) |
|
1151 |
|
1152 lemma abs_less_iff: |
1148 lemma abs_less_iff: |
1153 "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" |
1149 "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" |
1154 by (simp add: less_le abs_le_iff) (auto simp add: abs_if) |
1150 by (simp add: less_le abs_le_iff) (auto simp add: abs_if) |
1155 |
1151 |
1156 lemma abs_mult_pos: |
1152 lemma abs_mult_pos: |