src/HOL/Complex.thy

   by (simp add: rcis_def cis_def)
 
 lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
   by (simp add: rcis_def cis_def)
 
-lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
-proof -
-  have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
-    by (simp only: power_mult_distrib right_distrib)
-  thus ?thesis by simp
-qed
-
 lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
   by (simp add: rcis_def cis_def norm_mult)
 
 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
   by (simp add: cmod_def power2_eq_square)