Review on Decision Procedure on Linear Arithmetic

This is about the review of topics that De Moura covered in SSFT2013.

1. Here is my implementation on Sturm's Theorem in Univariate Polynomial case:

https://github.com/yihming/algebraic_geometry

    The language I choose is Haskell.

2. Here is my proof of Sturm's Theorem: