Coquand, T., Mörtberg, A. and Siles, V. (2012) “A formal proof of Sasaki-Murao algorithm”, Journal of Formalized Reasoning, 5(1), pp. 27–36. doi: 10.6092/issn.1972-5787/2615.