# HG changeset patch
# User chaieb
# Date 1203935220 -3600
# Node ID ca578d3b9f8cd228d54183ab15644167537a3186
# Parent  159afd21502f3e9d069f5af30f45c82205fdafd8
Added trivial theorems aboud cmod

diff -r 159afd21502f -r ca578d3b9f8c src/HOL/Complex/Complex.thy
--- 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 *}