##
Exercise 1

Try to define a next function over 'I_n that correspond to the
successor function over the natural plus the special case that
n -1

is mapped to zero

##
Exercise 2

Show that injectivity is decidable for a function f : aT -> rT
with aT a finite

##
Exercise 3

Try to formalize the following problem

Given a parking where the boolean indicates if the slot is occupied or not

Number of cars at column j

Show that if 0 < n there is always two lines, or two columns, or a column and a line
that have the same numbers of cars

##
Exercise 4

Prove the following state by induction and by following Gauss proof.

##
Exercise 7

Prove the following state by induction and by using a similar trick
as for Gauss noticing that n ^ 3 = n * (n ^ 2)

##
Exercise 8

building a monoid law