We define the floor function and the floor_ring instance on ℚ.
rat, rationals, ℚ, floor
floor q is the largest integer z such that z ≤ q