--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Apr 04 16:43:47 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 03 23:51:52 2014 +0100
@@ -998,7 +998,7 @@
f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))"
- using Suc by simp
+ using Suc by (simp add: divide_minus_left)
also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
proof -
have "of_nat(fact(Suc n)) *