Interactive Theorem Proving - Ayala-Rincón, Mauricio (Springer International Publishing, 2020)