src/HOL/Rings.thy
changeset 62347 2230b7047376
parent 61944 5d06ecfdb472
child 62349 7c23469b5118
--- a/src/HOL/Rings.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -1562,6 +1562,14 @@
 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: split_if_asm)
 
+lemma sum_squares_ge_zero:
+  "0 \<le> x * x + y * y"
+  by (intro add_nonneg_nonneg zero_le_square)
+
+lemma not_sum_squares_lt_zero:
+  "\<not> x * x + y * y < 0"
+  by (simp add: not_less sum_squares_ge_zero)
+
 end
 
 class linordered_ring_strict = ring + linordered_semiring_strict
@@ -1867,6 +1875,10 @@
   "sgn a < 0 \<longleftrightarrow> a < 0"
   unfolding sgn_if by auto
 
+lemma abs_sgn_eq:
+  "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
+  by (simp add: sgn_if)
+
 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)