Number-Theoretic Transform specification

[atrieu]

This is a new version of #1997 using the suggestions given there for specifying the NTT.

Specifically, this provides

• a theory of univariate polynomials (src/NTT/Polynomial.v)
• the algebraic form of the Chinese Remainder Theorem for polynomials (src/NTT/PolynomialCRT.v)
• explicit formulas for computing the CRT when the polynomial modulus has the form X^2 - a^2 (src/NTT/PolynomialCRT.v)
• the NTT as recursive applications of the CRT, also proved a ring isomorphism (src/NTT/NTT.v)
• lower level Gallina code implementing the NTT that is proved correct and should be more amenable to code generation (src/NTT/GallinaNTT.v)