ord_compl:

Add and prove cast_ord_incrF, filterP_cast_ord_incrF.

Finite_family:
WIP: filterP_ord_incrF (modified, use new incrF_Rg_eq_eq).
Modify filterP_f_ord_incrF.