Refinement of MathComp matrices and matrix operations

[palmskog]

For doing computation inside Coq using matrices, the most efficient way is likely as operations on Coq's primitive arrays. However, to make the connection to abstract MathComp matrices, there needs to be a refinement from them down to primitive arrays of arrays (e.g., via the refinement to lists of lists).

Suggested by a problem faced by @spitters.

[palmskog]

Another project that looks at the problem of efficient matrix computation, and is now also licensed under the MIT license: https://github.com/zhengpushi/coq-matrix

Might be possible to integrate some of the approaches into CoqEAL.