Please suggest example file for Coq Platform "smoke test kit"

[MSoegtropIMC]

I just added math-classes to Coq Platform (sorry for the long delay). In Coq Platform we have a so called "smoke test kit", which runs one or two example files from each package in order to test if the package has been properly installed. The example should test as much as possible, but shouldn't run longer than a few seconds (<10). Can you please suggest one or two files for this purpose?

Preferably the files should run with math-classes installed via opam without patching require statements and without -Q or -R options.

[spitters]

Perhaps take the files at the bottom of these hierarchies: https://math-classes.github.io/

E.g. https://github.com/coq-community/math-classes/blob/master/theory/dec_fields.v https://github.com/coq-community/math-classes/blob/master/interfaces/orders.v