如何在Coq中为实数定义"小于"？

我只是想知道如何为实数定义"小于"关系.

我理解,对于自然数(nat),<可以用一个数字作为另一个数字的(1+)后继者递归地定义S.我听说很多关于实数的事情在Coq中是公理化的而且没有计算.

但我想知道Coq中的实数是否存在最小公理集,基于哪些属性/关系可以导出.(例如 Coq.Reals.RIneq让它Rplus_0_r : forall r, r + 0 = r.成为公理,等等)

特别是,我很感兴趣,是否如关系<或<=可以在平等关系的顶部进行定义.例如,我可以想象在常规数学中,给出两个数字r1 r2:

r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2.

但这是否符合Coq的建设性逻辑？我是否可以用它来至少对不平等做一些推理(而不是一直重写公理)？