We define floor, ceil, and nat_ceil functions on linear ordered rings.
rounding
A floor_ring is a linear ordered ring over α with a function floor : α → ℤ satisfying ∀ (z : ℤ) (x : α), z ≤ floor x ↔ (z : α) ≤ x).
floor x is the greatest integer z such that z ≤ x
The fractional part fract r of r is just r - ⌊r⌋
ceil x is the smallest integer z such that x ≤ z
nat_ceil x is the smallest nonnegative integer n with x ≤ n. It is the same as ⌈q⌉ when q ≥ 0, otherwise it is 0.