Grimm, J. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. JFR 2016, 9, 1-52.