T. Coquand, A. Mörtberg, and V. Siles, “A formal proof of Sasaki-Murao algorithm”, JFR, vol. 5, no. 1, pp. 27–36, Jan. 2012.