  Integration, just as much as differentiation, is a fundamental calculus tool
that is widely used in many scientific domains. Formalizing the mathematical
concept of integration and the associated results in a formal proof assistant
helps providing the highest confidence on the correction of numerical programs
involving the use of integration, directly or indirectly. By its capability to
extend the (Riemann) integral to a wide class of irregular functions, and to
functions defined on more general spaces than the real line, the Lebesgue
integral is considered as perfectly suited for use in mathematical fields such
as probability theory, numerical mathematics, and real analysis. In this
article, we present the Coq formalization of $\sigma$-algebras, measures,
simple functions, and integration of nonnegative measurable functions, up to
the full formal proofs of the Beppo Levi (monotone convergence) theorem and
Fatou's lemma. More than a plain formalization of known literature, we present
several design choices made to balance the harmony between mathematical
readability and usability of Coq theorems. These results are a first milestone
towards the formalization of $L^p$~spaces such as Banach spaces.
