C. Sacerdoti Coen and E. Tassi, “A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita”, JFR, vol. 1, no. 1, pp. 51–89, Jan. 2008.