coq - Coq 中的 `Reals` 和 `Coq.Reals.*` 有什么区别？

Question

Reals在证明不等式和多项式方程等一般事实时，导入和类似的东西有什么区别Coq.Reals.{Rineq, R_sqrt, ...}？

我从搜索特定事实/定理开始，最终使用后者，但我看到其他人只使用Reals. 仅使用它更容易或更全面Reals吗？

怀疑它是遗留的东西，我试图导入，Coq.Reals但它似乎不存在（Coq 8.5 beta 3）。