affeldt-aist

> @affeldt-aist in fact, since #956 we have a Nix CI overlay that tests it (long story short: they moved to dune in graph-theory master, which made `make` build unconditionally...

This PR was discussed during the last MathComp meeting (https://github.com/math-comp/math-comp/wiki/Minutes-January-11-2023) and has been considered for merging. @JasonGross Could you rebase it? Thank you.

This check has been done for MathComp 1.18.0.

Would it be just a matter to add a `Make` file to the directory `all`?

It looks like users are now using `?lem//` to say that this is the subgoals generated by this rewriting that are discharged so the number of characters is not the...

TODO: find where to put this alternative proof in math-comp (gallery?)

Use `mczify` as a replacement for `lia`.

This seems to have been resolved by PR #763, please reopen if not.

The PR #990 has introduced similar lemma using the `\subset` notation for `finType` but not with the `{subset _

This issue seems to be solved by the new algebra-tactics package, so we close, please reopen if we are mistaken.