J. Grimm, “Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers”, JFR, vol. 9, no. 2, pp. 1–52, Jan. 2016.