[STATEMENT]
lemma summable_diff: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n - g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>summable f; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. f n - g n)
[PROOF STEP]
unfolding summable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ex ((sums) f); Ex ((sums) g)\<rbrakk> \<Longrightarrow> Ex ((sums) (\<lambda>n. f n - g n))
[PROOF STEP]
by (auto intro: sums_diff)