  ML4PG is a machine-learning extension that provides statistical proof hints
during the process of Coq/SSReflect proof development. In this paper, we use
ML4PG to find proof patterns in the CoqEAL library -- a library that was
devised to verify the correctness of Computer Algebra algorithms. In
particular, we use ML4PG to help us in the formalisation of an efficient
algorithm to compute the inverse of triangular matrices.
