Added trivial theorems aboud cmod

--- a/src/HOL/Complex/Complex.thy	Mon Feb 25 11:26:59 2008 +0100
+++ b/src/HOL/Complex/Complex.thy	Mon Feb 25 11:27:00 2008 +0100
@@ -338,6 +338,11 @@
 
 lemmas real_sum_squared_expand = power2_sum [where 'a=real]
 
+lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
+by (cases x) simp
+
+lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
+by (cases x) simp
 
 subsection {* Completeness of the Complexes *}