Add missing imports.
iota -> Hierarchy.iota.

Make some explicit...

Ropp_div -> Rdiv_opp_l
LM is compiling with Coq-8.20! (with no warning!)

       cont_lin_map -> clm,
       lin_map_ | _lin_map -> lm_ | lm_,
       lin_comb_ | _lin_comb | lin_comb2 -> lc_ | _lc | lc2,
       aff_map_ | _aff_map -> am_ | _am,
       aff_comb_ | _aff_comb -> ac_ | _ac,

       is_bilinear_mapping -> bilin_map,
       is_bounded_linear_mapping -> bound_lin_map,
       continuous_linear_map -> cont_lin_map,
       is_bounded_bilinear_mapping -> bound_bilin_map,
       is_bilinear_form -> bilin_form,
       is_sol_linear_pb -> sol_lin_pb.

Add AbelianMonoid stage in the hierarchy.
Use rewrite/apply from SSReflect when necessary.

check_sub_structure:
Obsolete, use FEM/Linalg/Sub_struct.

Rename compatible_m -> compatible_ms (_m is reserved for monoids).

FEM/_CoqProject:
Order.

FEM/Linalg_compl:
Prepare for possible add of monoids to the Coquelicot hierarchy.
Shorten some proofs.
Rename compatible_g_*_closed -> compatible_g_*,
       inhabited_m -> inhabited_ms.
Add def zero_closed.
Add sections on rings with many lemmas.
Some cosmetics.

FEM/Finite_table:
Shorten some proofs.

FEM/*.v:
Propagate new API (from LM and Linalg_compl).