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