Examples include the integers, the rationals and the real numbers.
In analogy with the real numbers, we call an element c of an ordered ring R positive if 0 < c, and negative if c < 0.
The set of positive elements of an ordered ring R is often denoted by R+.
The integers are a discrete ordered ring, but the rational numbers are not.
For all a, b and c in R: The list below includes references to theorems formally verified by the IsarMathLib project.