exercise2
This is the doc of seq, use it!
Exercise 1:
Exercise 1:
- 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
