Add a computable version of sturm sequences

This adds a computable definition of Sturm sequences, and an implementation of polynomial long division. The correctness proof of the sturm sequence equivalence is cheated for now, but we need it to define a mock-up checker and progress further with other tasks.