Let $R$ be an ordered integral domain, and let $inj: \mathbb{Z}_{+} \to R$ be the injection of the positive integers$\mathbb{Z}_{+}$ into $R$. $R$ is an Archimedean ordered integral domain if there is a family of dependent terms

$a:R, b:R \vdash \alpha(a, b): ((0 \lt a) \times (0 \lt b)) \to \Vert \sum_{n:\mathbb{Z}_{+}} a \lt inj(n) \cdot b \Vert$

Examples

The integers are an Archimedean ordered integral domain.