> I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not. It would work with Coq's real number type but as

> I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not. It would work with Coq's real number type but as the same properties wouldn't always hold with hardware float types, you may have trouble running the program if you extracted it to e.g. Haskell (as your example shows)? The QuickCheck tests would pass if you allowed a small difference between them to account for floating point inaccuracies I imagine.