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.

what follows is a slide, it creates an index item next to the scroll bar,
just move the mouse there.

#
Induction and structured proofs

###
Exercise 1

Let us prove directly formula
\[ \sum_{i=0}^{n-1} (2 i + 1) = n ^ 2 \]
from lesson 1, slightly modified.

Let us first recall custom sum operator:

- First prove a very useful lemma about
`iota` (you can use `iota_add`) (Easy)

- Then prove a very useful lemma about summation. (Medium)

- Now use the previous result to get the main result (Easy - Medium)

###
Exercise 2

Prove that the equation \[ 8y = 6x + 1 \] has no solution. (Easy)

- Hint 1: take the modulo 2 of the equation (using
`suff`).
- Hint 2:
`Search _ "contra" in MC` and use the view `eqP`.
- Hint 3:
`Search _ modn addn in MC` and `Search _ modn muln in MC`

###
Exercise 3:

The ultimate Goal of this exercise is to find the solutions of the equation
\[ 2^n = a^2 + b^2,\] where n is fixed and a and b unkwown.
We hence study the following predicate:

- We give the set of solutions for \(n = 0\) or \(1\)

- Now prove a little lemma that will guarantee that a and b are even. (Medium - Hard)
- Hint:
`Search _ (_ ^ 2) (_ + _) in MC`.
- Hint:
`Search ((_ * _) ^ _) in MC`.
- ...
- Hint:
`About divn_eq` to substitute a and b (rewrite {1}(div_eq ...))
- Hint:
`Search _ modn odd in MC`.

- Do it on paper first!

- Deduce that if n is greater than 2 and a and b are solutions, then they are even. (HARD)

- Prove that the solutions for n are the halves of the solutions for n + 2.
- Hint:
`Search _ odd double in MC` and `Search _ "eq" "mul" in MC`.

- Prove there are no solutions for n even (Easy)
- Hint: Use
`sol0` and `solSS`.

- Certify the only solution when n is odd. (SUPER HARD)
- Hint 1: Use
`sol1`, `solSS` and `sol_are_even`.
- Hint 2: Really sketch it on paper first!