Coquand, Thierry, Anders Mörtberg, and Vincent Siles. “A Formal Proof of Sasaki-Murao Algorithm”. Journal of Formalized Reasoning 5, no. 1 (January 1, 2012): 27–36. Accessed October 3, 2023. https://jfr.unibo.it/article/view/2615.