Deducteam · fblanqui · Jan 11, 2025 · Jan 11, 2025 · Jan 11, 2025 · Jan 11, 2025
diff --git a/Logic.v b/Logic.v
diff --git a/README.md b/README.md
@@ -5,7 +5,7 @@ This library provides a translation in Coq of the definition of real numbers in
 
 It has been automatically generated from HOL-Light using [hol2dk](https://github.com/Deducteam/hol2dk) and [lambdapi](https://github.com/Deducteam/lambdapi).
 
-Proofs are not included but can be regenerated and rechecked by running [reproduce](https://github.com/Deducteam/coq-hol-light-real/blob/main/reproduce) (it takes around 5 minutes on a machine with 32 processors Intel Core i9-13950HX and 64 Gb RAM).
+Proofs are not included but can be regenerated and rechecked by running [reproduce](https://github.com/Deducteam/coq-hol-light-real/blob/main/reproduce) (it takes about 7 minutes on a machine with 32 processors Intel Core i9-13950HX and 64 Gb RAM).
 
 As HOL-Light is based on higher-order logic, this library assumes classical logic, Hilbert's ε operator, functional and propositional extensionnality (see [HOLLight.v](https://github.com/Deducteam/coq-hol-light-real/blob/main/HOLLight.v) for more details):
 

diff --git a/With_N.v b/With_N.v