diff -r 85ed00c1fe7c -r 340738057c8c src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Series.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -390,6 +390,9 @@
     by (simp add: ac_simps)
 qed simp
 
+corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s"
+  by (simp add: sums_iff_shift)
+
 lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
   by (metis diff_add_cancel summable_def sums_iff_shift[abs_def])
 
@@ -535,6 +538,12 @@
 lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
 
+lemma sums_mult_D: "\<lbrakk>(\<lambda>n. c * f n) sums a; c \<noteq> 0\<rbrakk> \<Longrightarrow> f sums (a/c)"
+  using sums_mult_iff by fastforce
+
+lemma summable_mult_D: "\<lbrakk>summable (\<lambda>n. c * f n); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f"
+  by (auto dest: summable_divide)
+
 text\<open>Sum of a geometric progression.\<close>
 
 lemma geometric_sums: "norm c < 1 \<Longrightarrow> (\<lambda>n. c^n) sums (1 / (1 - c))"