Coquand, T.; Mörtberg, A.; Siles, V. A Formal Proof of Sasaki-Murao Algorithm. JFR 2012, 5, 27-36.