Coquand, Thierry, et al. “A Formal Proof of Sasaki-Murao Algorithm”. Journal of Formalized Reasoning, vol. 5, no. 1, Jan. 2012, pp. 27-36, doi:10.6092/issn.1972-5787/2615.