Interactive Theorem Proving - Jeremy Avigad, Assia Mahboubi (Springer International Publishing, 2018)