Coquand, Thierry, Anders Mörtberg, and Vincent Siles. 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.