Function_compl:

Make *explicit* some arguments!

Finite_family:
Add and prove incrF_inj.
Rename injF_restr_bij_EX -> injF_restr_bij_EX' (should be removed).
Add new def injF_restr_bij_EX (simpler).
Add and prove  extendPF_incrF.
WIP: filterP_ord_incrF.
Rename, move and prove filterP_f_ord_incr -> filterP_f_ord_incrF.
Adapt filter*_unfunF* to new def injF_restr_bij_EX.

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