[STATEMENT]
lemma suffix_conc_snd[simp]:
  assumes "n \<ge> length u"
  shows "suffix n (u \<frown> v) = suffix (n - length u) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix n (u \<frown> v) = suffix (n - length u) v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. suffix n (u \<frown> v) x = suffix (n - length u) v x
[PROOF STEP]
show "suffix n (u \<frown> v) i = suffix (n - length u) v i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix n (u \<frown> v) i = suffix (n - length u) v i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length u \<le> n

goal (1 subgoal):
 1. suffix n (u \<frown> v) i = suffix (n - length u) v i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
suffix n (u \<frown> v) ?i = suffix (n - length u) v ?i

goal:
No subgoals!
[PROOF STEP]
qed