--- a/src/HOL/Complex/NSComplex.thy Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy Tue Jan 06 10:40:15 2004 +0100
@@ -481,6 +481,13 @@
by (rule hcomplex_zero_not_eq_one)
show "(u + v) * w = u * w + v * w"
by (simp add: hcomplex_add_mult_distrib)
+ show "z+u = z+v ==> u=v"
+ proof -
+ assume eq: "z+u = z+v"
+ hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
+ thus "u = v"
+ by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
+ qed
assume neq: "w \<noteq> 0"
thus "z / w = z * inverse w"
by (simp add: hcomplex_divide_def)