Reorganize the test-suite and examples

[pi8027]

Files in examples/ have two roles:

• examples showing the features of Algebra Tactics, and
• test-suite.

I see the following three issues:

• Currently, these two things are kind of mixed. So, they are not very friendly to the users who want to discover the features.
• Checking ring_examples.v and field_examples.v requires uncommenting Require Imports. (This way we can test the "no check" option.)
• As the test suite, they are not very exhaustive either.