compalg

Providing comparison functions between numbers that are sums of a rational number and a square root, with proofs in Coq+mathematlcal components