ord_compl:

Move stuff around.
Move extF_liftF_S, Rg_0_liftF_S, incrF_Rg_le_0, fun_ext_incrF_Rg from Finite_family.
Rename narrow_S_inj -> narrow_S_injS,
       lower_S_inj -> lower_S_injS.
Add def nondecrF.
Add and prove bump_{eq,neq,incr},
              sortedF_monot, incrF_nondecrF,
              narrow_S_inj, lower_S_inj,
              {widen,lift}_S_incrF, {narrow,lower}_S_incr{F,S}.
Generalize filterP_cast_ord_incrF to any m (instead of 'I_n1).
Alternate proof of filterP_ord_ind_l_in_n0 not using lower-level stuff from MC.

Finite_family:
Move extF_liftF_S, Rg_0_liftF_S, incrF_Rg_le_0, fun_ext_incrF_Rg to ord_compl.