Function_sub:

Add and prove Rg_comp_alt.

ord_compl:
Move stuff around.
Make some arguments explicit, others implicit.
Add and prove ord0_equiv_le, ord_n0_equiv_gt,
              incrF_{0,max},
              cast_ord0_equiv_le{q,}, cast_ord_n0_equiv_gt{n,},
              incrF_cast_ord_{0,max},
              filterP_ord_incl_Rg, filterP_ord_Rg_eq.
Simplify proofs of filterP_ord_ind_l_in_0{,_rev}.
Btw, filterP_rev_ord seems OK!

Finite_family:
Propagate new API (from ord_compl).