Prove properties of rounding functions in Data.Rational(.Unnormalised).Base

[MatthewDaggitt]

Follow up to #1063, which was partially addressed in #1585. Once the properties have been proved, there's an argument that we can remove the test suite added in #1585, though I'm open to counter-arguments for keeping it...

[barrettj12]

Some examples of properties that we might like to prove for each of floor, ceiling, truncate, round:

• Monotonicity: floor p ≤ p*, ceiling p ≥ p, | truncate p | ≤ p, | round p - p | ≤ ½
• That each one is the "optimal" integer satisfying the above, e.g. (z : ℤ) → z ≤ p → z ≤ floor p, (z : ℤ) → | round p - p | ≤ | z - p |
• Identity on integers, e.g. (z : ℤ) → floor z ≡ z (and maybe converses?)
• Symmetry and relations between them: floor (- p) ≡ - (ceiling p), truncate p ≡ truncate (- p), round p ≡ round (- p)

* I'm convinced this one needs [n/d]*d≤n from Data.Integer.DivMod, but I can't work it out.

[MatthewDaggitt]

In my opinion I think the relationships between the number being rounded and the result of rounding, e.g. floor p + fracPart p ≡ p and 0 ≤ fracPart x < 1 are the most important. The rest should all be derivable from those.