- use no lemma to prove the following statement

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

- look for lemmas supporting contrapositive reasoning

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

- 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`

- prove that using
`case:` - then prove that without using case:

- look up the definition of
`iter` - prove this tatement by induction

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

- 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) = ...

- 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