Interactive Theorem Proving - Ayala-Rincón; Muñoz, César A. (Springer International Publishing, 2017)