Address deprecation warnings and clean up the import lists

[pi8027]

This PR is intended to be compatible with math-comp/math-comp#1237 (not tested yet).

The import lists are now in the dependency order, except for some stuff imported in the middle of a file.

[pi8027]

I should probably do a benchmark tomorrow, just in case.

[pi8027]

Performance comparison of before/after this PR:

    After |   Peak Mem | File Name                     |    Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------
21m51.61s | 1660244 ko | Total Time / Peak Mem         | 21m49.03s | 1662328 ko || +0m02.58s ||     -2084 ko |   +0.19% |         -0.12%
----------------------------------------------------------------------------------------------------------------------------------------
 4m44.59s |  880552 ko | PFsection4.vo                 |  4m41.74s |  898192 ko || +0m02.85s ||    -17640 ko |   +1.01% |         -1.96%
 3m28.72s | 1650756 ko | PFsection9.vo                 |  3m29.14s | 1654544 ko || -0m00.42s ||     -3788 ko |   -0.20% |         -0.22%
 1m03.78s | 1035636 ko | PFsection13.vo                |  1m03.75s | 1042704 ko || +0m00.03s ||     -7068 ko |   +0.04% |         -0.67%
 0m53.58s |  990468 ko | PFsection12.vo                |  0m53.80s |  990612 ko || -0m00.22s ||      -144 ko |   -0.40% |         -0.01%
 0m49.48s | 1043408 ko | PFsection11.vo                |  0m49.35s | 1056652 ko || +0m00.13s ||    -13244 ko |   +0.26% |         -1.25%
 0m46.38s | 1100932 ko | BGsection14.vo                |  0m46.29s | 1090056 ko || +0m00.09s ||     10876 ko |   +0.19% |         +0.99%
 0m43.64s |  885928 ko | BGsection12.vo                |  0m43.33s |  885912 ko || +0m00.31s ||        16 ko |   +0.71% |         +0.00%
 0m41.14s |  977784 ko | PFsection10.vo                |  0m41.05s |  977272 ko || +0m00.09s ||       512 ko |   +0.21% |         +0.05%
 0m40.27s |  962468 ko | PFsection6.vo                 |  0m40.44s |  972612 ko || -0m00.17s ||    -10144 ko |   -0.42% |         -1.04%
 0m36.61s |  939932 ko | PFsection14.vo                |  0m36.74s |  954548 ko || -0m00.13s ||    -14616 ko |   -0.35% |         -1.53%
 0m35.88s |  851836 ko | BGappendixC.vo                |  0m35.91s |  869080 ko || -0m00.03s ||    -17244 ko |   -0.08% |         -1.98%
 0m34.61s |  832108 ko | BGsection16.vo                |  0m34.11s |  828724 ko || +0m00.50s ||      3384 ko |   +1.46% |         +0.40%
 0m33.83s |  859520 ko | BGsection15.vo                |  0m34.02s |  863240 ko || -0m00.19s ||     -3720 ko |   -0.55% |         -0.43%
 0m33.79s |  895048 ko | BGsection3.vo                 |  0m34.01s |  894760 ko || -0m00.22s ||       288 ko |   -0.64% |         +0.03%
 0m33.66s |  928484 ko | PFsection5.vo                 |  0m33.94s |  930024 ko || -0m00.28s ||     -1540 ko |   -0.82% |         -0.16%
 0m27.51s |  928592 ko | PFsection3.vo                 |  0m27.60s |  930108 ko || -0m00.09s ||     -1516 ko |   -0.32% |         -0.16%
 0m22.07s | 1660244 ko | BGappendixAB.vo               |  0m22.20s | 1662328 ko || -0m00.13s ||     -2084 ko |   -0.58% |         -0.12%
 0m20.29s |  881652 ko | PFsection7.vo                 |  0m20.34s |  881092 ko || -0m00.05s ||       560 ko |   -0.24% |         +0.06%
 0m19.79s |  861200 ko | PFsection8.vo                 |  0m19.87s |  861564 ko || -0m00.08s ||      -364 ko |   -0.40% |         -0.04%
 0m19.70s |  848320 ko | wielandt_fixpoint.vo          |  0m19.67s |  848420 ko || +0m00.03s ||      -100 ko |   +0.15% |         -0.01%
 0m19.51s |  789184 ko | BGsection13.vo                |  0m19.35s |  787468 ko || +0m00.16s ||      1716 ko |   +0.82% |         +0.21%
 0m18.97s |  780684 ko | BGsection10.vo                |  0m18.93s |  783252 ko || +0m00.04s ||     -2568 ko |   +0.21% |         -0.32%
 0m18.47s |  800824 ko | BGsection4.vo                 |  0m18.38s |  801056 ko || +0m00.09s ||      -232 ko |   +0.48% |         -0.02%
 0m17.81s |  809728 ko | BGsection2.vo                 |  0m17.76s |  806632 ko || +0m00.05s ||      3096 ko |   +0.28% |         +0.38%
 0m14.48s |  824928 ko | PFsection1.vo                 |  0m14.52s |  837672 ko || -0m00.04s ||    -12744 ko |   -0.27% |         -1.52%
 0m13.85s |  757312 ko | BGsection7.vo                 |  0m13.87s |  757948 ko || -0m00.02s ||      -636 ko |   -0.14% |         -0.08%
 0m12.45s |  750216 ko | BGsection1.vo                 |  0m12.39s |  752616 ko || +0m00.06s ||     -2400 ko |   +0.48% |         -0.31%
 0m10.55s |  803504 ko | PFsection2.vo                 |  0m10.53s |  801736 ko || +0m00.02s ||      1768 ko |   +0.18% |         +0.22%
 0m09.03s |  728652 ko | BGsection5.vo                 |  0m08.94s |  724972 ko || +0m00.09s ||      3680 ko |   +1.00% |         +0.50%
 0m07.92s |  724508 ko | BGsection8.vo                 |  0m07.85s |  725396 ko || +0m00.07s ||      -888 ko |   +0.89% |         -0.12%
 0m06.06s |  722968 ko | BGsection9.vo                 |  0m05.98s |  724956 ko || +0m00.08s ||     -1988 ko |   +1.33% |         -0.27%
 0m05.25s |  729624 ko | BGsection11.vo                |  0m05.27s |  729764 ko || -0m00.02s ||      -140 ko |   -0.37% |         -0.01%
 0m04.56s |  718868 ko | BGsection6.vo                 |  0m04.57s |  718808 ko || -0m00.01s ||        60 ko |   -0.21% |         +0.00%
 0m03.38s |  824576 ko | stripped_odd_order_theorem.vo |  0m03.39s |  820980 ko || -0m00.01s ||      3596 ko |   -0.29% |         +0.43%

I'm merging this PR now since the difference is negligible.