Reduce the number of `From mathcomp Require Import`

What about writing:
```coq
From mathcomp Require Import blah0 blah1 blah2.
```
instead of
```coq
From mathcomp Require Import blah0.
From mathcomp Require Import blah1.
From mathcomp Require Import blah2.
```
?
We could spare a few lines while keeping the 80 characters width constraint.
Maybe there is a technical reason?
