Removing dependency on mathcomp

[raoxiaojia]

As far as I'm aware, only the ssreflect part of mathcomp is used in the repository, which is now meregd into base Coq (as of version 8.18). So it makes sense to remove the dependency on it to avoid dealing with the slightly awkward CeCILL-B license (discovered in #29).

[palmskog]

@raoxiaojia looking around the codebase, it's pretty clear that you are using significant pieces of mathcomp-ssreflect that are not in Coq itself. The general idea is that the proof language SSReflect is in Coq, but most theories except for booleans is outside of Coq in MathComp.

Specifically, the theories here are defining canonical structures with decidable equality (eqType) and using MathComp sequences/lists and their notations (seq). This would be work to remove, just to avoid the CECILL-B licensing issues (which are basically only triggered by GPLv2 and GPLv3, which are not common in the Coq ecosystem).

cc: @spitters

[raoxiaojia]

That is true -- I had some thoughts about eqTypes and other things, but haven't realised that their lists (seq) are also not in base Coq. I guess this is too low a priority for now then.