[STATEMENT]
lemma ltake_plus_conv_lappend:
  "ltake (n + m) xs = lappend (ltake n xs) (ltake m (ldrop n xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake (n + m) xs = lappend (ltake n xs) (ltake m (ldrop n xs))
[PROOF STEP]
by(coinduction arbitrary: n m xs rule: llist.coinduct_strong)(auto intro!: exI simp add: iadd_is_0 ltl_ltake epred_iadd1 ldrop_ltl)