src/HOL/Transcendental.thy
changeset 57129 7edb7550663e
parent 57025 e7fd64f82876
child 57180 74c81a5b5a34
     1.1 --- a/src/HOL/Transcendental.thy	Fri May 30 12:54:42 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Fri May 30 14:55:10 2014 +0200
     1.3 @@ -76,10 +76,7 @@
     1.4  lemma lemma_realpow_rev_sumr:
     1.5     "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
     1.6      (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
     1.7 -  apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
     1.8 -  apply (auto simp: image_iff Bex_def intro!: inj_onI)
     1.9 -  apply arith
    1.10 -  done
    1.11 +  by (subst nat_diff_setsum_reindex[symmetric]) simp
    1.12  
    1.13  lemma power_diff_1_eq:
    1.14    fixes x :: "'a::{comm_ring,monoid_mult}"