[STATEMENT]
lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq f"
  for f :: "nat \<Rightarrow> 'a::real_normed_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bseq (\<lambda>x. f x + c) = Bseq f
[PROOF STEP]
using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"]
[PROOF STATE]
proof (prove)
using this:
Bseq f \<Longrightarrow> Bseq (\<lambda>x. f x + c)
Bseq (\<lambda>x. f x + c) \<Longrightarrow> Bseq (\<lambda>x. f x + c + - c)

goal (1 subgoal):
 1. Bseq (\<lambda>x. f x + c) = Bseq f
[PROOF STEP]
by auto