###
Exercices on polynomials

- Formalisation of the algebraic part of a
simple proof that PI is irrational described in:
- http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788

###
Parameters definitions:

- Let n na nb be natural numbers
- Suppose nb is a non zero nat: nb != 0
- Define the corresponding rationals a , b
- Define pi as a/b.

###
Definition of the polynomials:

- Look at the f definition: the factorial, the coercion nat :> R (as a Ring), etc...
- Define F:{poly rat} using bigop.

###
Prove that:

- the lead_coef of (a - bX) is -b.

###
Prove that:

- the size of (a-X)^n is n.+1

###
Prove that:

- Exponent and composition of polynomials combine:

###
Prove that:

- f's small coefficients are zero

###
Prove that:

- f/n! as integral coefficients

###
Prove that:

the f^`(i) (x) have integral values for x = 0

###
Deduce that:

F (0) has an integral value

###
Then prove

- the symmetry argument f(x) = f(pi -x).

###
Prove

- the symmetry for the derivative

###
if you have time

- you can prove the equality F^`(2) + F = f
- that is needed by the analytic part of the Niven proof