Consolidation after inclusion of matrix canonical forms

[palmskog]

After #54 is merged, we need to consolidate some material and possibly reorganize it a bit. I open this issue as a memento.

So far, we have at least the following mentioned by Cyril:

the companion matrix has been added to mathcomp already.

[proux01]

We could also clean a bit the ssrcomplement file, once MathComp 1.13 is out and we switch to it.

[CohenCyril]

There should be some refactoring in about similar since the propositional definition is now in mathcomp. CoqEAL provides a decidability result that should establish a correspondence between propositional and boolean versions of similarity.