Textbook in PDF format This document is a memo written for a class of about ten hours held at the Graduate School of Mathematics at Nagoya University from [2022-12-19] to [2022-12-23]. The intent is to provide the necessary background about the Coq proof assistant and the MathComp library (for students who already had an exposition to these pieces of software) to be able to understand and get started with the MathComp-Analysis library. This document is meant to be selfcontained. Since Coq and MathComp are already explained elsewhere, the parts about them are rather cursory, relying on pointers to the appropriate literature such as the Coq reference manual [The Coq Development Team, 2024], the original SSReflect manual [Gonthier et al., 2016], and the Mathematical Components book [Mahboubi and Tassi, 2021]. And for Japanese readers: [Affeldt, 2017], [Hagiwara and Affeldt, 2018]