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 *:
- 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 5 ****:
- what is 'C() ?
- use lia.
- use eq_bigr (
- and look for the appropriate
telescope
lemma.