### Exercices on polynomials

• Formalisation of the algebraic part of a simple proof that PI is irrational described in:

### 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:

• b is non zero rational.

### Prove that:

• (a - bX) has a size of 2

### 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

### Deduce that

• F(pi) is an integer

### if you have time

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