# HG changeset patch
# User chaieb
# Date 1203935223 -3600
# Node ID cb9bdde1b444616f9f09c6f34e00a89a44d245e1
# Parent  6f94eb10adad290a5ae1725cb43bd3199e19bb64
Two simple theorems about cmod moved to Complex.thy

diff -r 6f94eb10adad -r cb9bdde1b444 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Mon Feb 25 11:27:02 2008 +0100
+++ b/src/HOL/Complex/NSCA.thy	Mon Feb 25 11:27:03 2008 +0100
@@ -245,11 +245,6 @@
 
 subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *}
 
-lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
-by (induct x) simp
-
-lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
-by (induct x) simp
 
 lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
 by transfer (rule abs_Re_le_cmod)