Coquand, T. et al. 2012. A formal proof of Sasaki-Murao algorithm. Journal of Formalized Reasoning. 5, 1 (Dec. 2012), 27–36. DOI:https://doi.org/10.6092/issn.1972-5787/2615.