Function_compl:

Rename f_inv_correct_{l,r} -> f_inv_can_{l,r}.

Function_sub:
Add def involS.
Add and prove involS_injS, involS_bijS.
Rename f_invS_canS_l <-> f_invS_canS_r.
Add and prove f_invS_uniq_{l,r}, f_invS_{bijS,injS,surjS},
              f_invS_eq_equiv, f_invS_neq_equiv,
              f_invS_ext, f_invS_invol{,_alt},
              f_invS_id{,_rev,_equiv}.

ord_compl, Finite_family, ModuleSpace_compl, AffineSpace, Finite_dim,
  poly_Lagrange, P_approx_k, FE_LagP:
Propagate new API (from Function_compl).

FE_LagP:
Propagate new API (from Function_sub).