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 4 ***:

  • 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 5 ****:

  • what is 'C() ?
  • use lia.
  • use eq_bigr (
  • and look for the appropriate telescope lemma.