A formal proof of Sasaki-Murao algorithm

The Sasaki-Murao algorithm computes the determinant of any square matrix over a commutative ring in polynomial time. The algorithm itself can be written as a short and simple functional program, but its correctness involves nontrivial mathematics. We here represent this algorithm in Type Theory with a new correctness proof, using the Coq proof assistant and the SSReflect extension.