remove no longer needed lemmas (as of mathcomp-1.11)

[chdoc]

No description provided.

[chdoc]

@palmskog , this drops mathcomp-1.9 and mathcomp-1.10`, but I think three versions of mathcomp are enough. If we make a release with theory changes, maybe it's a good idea to include this.

[palmskog]

@chdoc dropping 1.9 and 1.10 is perfectly fine by me, now that we have a release that is likely to work for a while on 1.13. Should I modify meta.yml and the CI configuration in the PR branch?

[chdoc]

@chdoc dropping 1.9 and 1.10 is perfectly fine by me, now that we have a release that is likely to work for a while on 1.13. Should I modify meta.yml and the CI configuration in the PR branch?

Yes, please do.

[chdoc]

As far as I am concerned, this is ready to be merged.

[palmskog]

Hmm, I think we could also bump to 8.15 compatibility, and add at least Nix CI for 8.15 (the MC 8.15 Docker images are not available yet). Or should we do 8.15 in a separate PR?

[chdoc]

I think that should be a separate PR. Also, I don't expect any changes to the .v files for 8.15, given that master checks just fine.