Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.

####
maxn defines the maximum of two numbers

####
We define the maximum of three number as folllows

####
Try to prove the following facts (you may use properties of maxn provided by the library)

###
Exercise 1

###

The next exercise consists in proving an alternative induction scheme on type list,
whose base case is the last element in the list.

For this purpose, we first define a concatenation operation between lists
and prove a few lemmas about it.

The 'rcons' operation is provided by the underlying library, and appends its
last argument to the end of its first, which is a list.

The exercise is self-contained : you should not use results that you did not
prove yourself.

###
Definition of the concatenation operation

###
Exercise 9.

####
(Hint: this proof does not require an induction step)

###
Exercise 10.

####
Prove lemma last_ind using first the intermediate lemma hcat,

and then by induction. Hint: use the lemmas you have proved
so far on function cat.