  Formalization of real analysis offers a chance to rebuild traditional proofs
of important theorems as unambiguous theories that can be interactively
explored. This paper provides a comprehensive overview of the Lebesgue
Differentiation Theorem formalized in the Coq proof assistant, from which the
first Fundamental Theorem of Calculus (FTC) for the Lebesgue integral is
obtained as a corollary. Proving the first FTC in this way has the advantage of
decomposing into loosely-coupled theories of moderate size and of independent
interest that lend themselves well to incremental and collaborative
development. We explain how we formalize all the topological constructs and all
the standard lemmas needed to eventually relate the definitions of derivability
and of Lebesgue integration of MathComp-Analysis, a formalization of analysis
developed on top of the Mathematical Components library. In the course of this
experiment, we substantially enrich MathComp-Analysis and even devise a new
proof for Urysohn's lemma.
