let rlt_URI = uri rlt_SURI
let rgt_SURI = "cic:/Coq/Reals/Rdefinitions/Rgt.con"
let rgt_URI = uri rgt_SURI
- let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
- let rinv_r1_URI = uri "cic:/Coq/Reals/Rbase/Rinv_R1.con"
+ let rtheory_URI = uri "cic:/Coq/Reals/RIneq/RTheory.con"
+ let rinv_r1_URI = uri "cic:/Coq/Reals/RIneq/Rinv_1.con"
let pow_URI = uri "cic:/Coq/Reals/Rfunctions/pow.con"
let r = const r_URI
let ge_URI = uri ge_SURI
let lt_SURI = "cic:/Coq/Init/Peano/lt.con"
let lt_URI = uri lt_SURI
- let gt_SURI = "cic:/Coq/Init/Peano/lt.con"
+ let gt_SURI = "cic:/Coq/Init/Peano/gt.con"
let gt_URI = uri gt_SURI
- let lt_URI = uri "cic:/Coq/Init/Peano/lt.con"
let plus = const plus_URI
let mult = const mult_URI