To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Exercise 1:

• look for lemmas supporting contrapositive reasoning
• use the eqP view to finish the proof.

Exercise 2:

• 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 3:

• Prove this view by unfolding maxn and then using leqP

Exercise 4:

• 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