Move stuff around.

Add and prove ord_max_equiv_ge{q,}, ord_nmax_equiv_lt{n,},
              cast_ord_max_equiv_ge{q,}, cast_ord_nmax_equiv_lt{n,},
              lenPF_ind_r_in_S_alt.
Higher-level proof of filterP_ord_ind_r_in_max.
WIP: filterP_ord_ind_r_in_max_rev.