Exercise 1:

• use no lemma to prove the following statement

Exercise 2:

• look up what ==> is check if there are relevant views
• prove that as you like

Exercise 3:

• look for lemmas supporting contrapositive reasoning

Exercise 4:

• what is (+) ?
• find the right view to prove this statement
• now find another proof without the view

Exercise 5:

• it helps to find out what is behind ./2 and .*2 in order to Search
• any proof would do, but there is one not using implyP

Exercise 6:

• prove that using case:
• then prove that without using case:

Exercise 7:

• look up the definition of iter
• prove this tatement by induction

Exercise 8:

• look up the definition of iter (note there is an accumulator varying during recursion)
• prove the following statement by induction

Exercise 9:

• the only tactics allowed are rewrite and by
• use Search to find the relevant lemmas (all are good but for ltn_neqAle) or browse the online doc
• proof sketch:
```        m < n = ~~ (n <= m)
= ~~ (n == m || n < m)
= n != m && ~~ (n < m)
= ...
```

Exercise 10:

• there is no need to prove reflect with iffP: here just use rewrite and apply
• check out the definitions and theory of leq and maxn
• proof sketch:
```   n <= m = n - m == 0
= m + n - m == m + 0
= maxn m n == m
```