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