src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56889 48a745e1bde7
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -998,7 +998,7 @@
     1.4             f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
     1.5             f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
     1.6             f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))"
     1.7 -        using Suc by (simp add: divide_minus_left)
     1.8 +        using Suc by simp
     1.9        also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
    1.10        proof -
    1.11          have "of_nat(fact(Suc n)) *