Port Coq code to use done tactic instead of easy and benchmark

Math Classes currently uses the easy tactic from Coq's standard library as a finisher tactic to close a goal. However, easy is known to be slow, most directly because it uses inversion. For example, it can be slow when there are inductives with many constructors in the proof context.

An alternative to easy is the done tactic from Coq-Std++, which does not use inversion, and incorporates best practices from the MathComp done tactic. Math Classes could likely benefit from being ported to use done instead of easy, which would be a good project for a first-time contributor. There should be benchmarks with and without done to measure the improvements.

The port should not necessarily make Math Classes depend on Coq-Std++, but could bundle the done tactic.

Search the Math Classes sources for uses of Coq's easy tactic and review how the project currently handles tactic dependencies. Compare the existing behavior with Coq-Std++'s done tactic, then add benchmarks with and without done so completion includes measured improvements.