Function_compl:

Add and prove f_inv_inj, f_inv_surj.

ord_compl, Finite_family, Monoid_compl, AffineSpace:
Propagate new API (from Function_compl).

Finite_family:
Add defs eqF, neqF (fold them everywhere).
Rename funF_neq -> funF_neqF (modified),
       unfunF_neq -> unfunF_neqF,
       extendPF_funF_neq -> extendPF_funF_neqF,
       extendPF_equiv -> extendPF_unfunF_equiv,
       extendPF_unfunF_neq -> extendPF_unfunF_neqF.
Add and prove funF_equiv,
              extendPF_funF_{rev,equiv},
              extendPF_funF_neqF_{rev,equiv}.
WIP: filterPF_funF.