This is the doc of seq, use it!

• look up the documentation of take and drop
• prove this by induction (mind the recursive argument)

Exercise 2:

• look at the definition of take and size and prove the following lemma
• the proof goes by cases

Exercise 3:

• another proof by cases

Exercise 4:

• Look up the definition of rot
• Look back in this file the lemma cat_take_drop
• can you rewrite with it right-to-left in the right-hand-side of the goal?

Exercise 5:

• which is the size of an empty sequence?
• Use lemmas about size and filter

Exercise 6:

• prove that by induction

Exercise 7:

• prove that view (one branch is by induction)

Exercise 8:

• induction once more

Exercise 9:

• prove this by induction on s