I think it should be in Chapter: Introduction Subchapter: Running examples in the Coq system The link is https://math-comp.github.io/mcb/snippets/