A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita