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.

Mv union_inj from Algebra.Finite_family to union_inj_r.
Add union_inj_l, inter_inj_{l,r}.

Finite_family:
Rename widenF_S_inj -> widenF_S_reg,
       liftF_S_inj -> liftF_S_reg,
       eqAF_0_liftF_S -> extF_liftF_S (modified).
Add and prove widenF_S_compat, eqxFn_equiv,
              widenF_S_nextF_compat, widenF_S_nextF_reg, neqxFn_equiv,
              extF_widenF_S,
              liftF_S_compat, eqxF0_equiv,
              liftF_S_nextF_compat, liftF_S_nextF_reg, neqxF0_equiv.
Mv union_inj to Compl.Subset_compl.union_inj_r.

Finite_dim:
Propagate new API (from Finite_family).

Add injS_equiv_seq (WIP).

Add and prove lt_ltn, le_leq.

ord_compl:
WIP: map_injS_uniq.
Add def in_ordS.
Add and prove nth_ord_enum_alt,
              in_ordS_correct_{l{,_alt},r}, val_in_ordS, in_ordS_injS,
              ord_enumS_eq.
Proof of perm_ord_enum_sort.

Finite_family:
Simplify proof.

Add and prove incrF_comp.
WIP: filterP_ord_incrF.

Finite_family:
Add and prove filterP_ord_Rg{_aux{1,2,3},}.

Add and prove nth_ord_enum.

Finite_family:
WIP: injF_restr_bij_EX, filterP_ord_incrF.

Add and prove inj_contra.

nat_compl:
Add and prove ltn_neq, leq_neq_ltn, ltn_leq_neq, ltn_equiv, ltn_S.
Rename ltS_neq_lt -> ltnS_neq_ltn (proof simplified).

ord_compl:
Propagate new API (from nat_compl).
Add and prove ord_leq_{refl,antisym,trans,total}.

Finite_family:
WIP: injF_restr_bij_EX.

Rename seq_* -> *, path_* -> *.
Move stuff around.
Make some arguments explicit.
Add and prove fun_from_I_0_inj, fun_from_I_0_bij.
Move Finite_family.seq_perm_eq_ex -> perm_EX (modified = fixed),
     Finite_family.seq_sort_perm_ex -> sort_perm_EX (modified = fixed),
     def incrF, incrF_inj, ord_leq from Finite_family.
WIP: sort_perm_EX.

Finite_family:
Move def incrF, incrF_inj, ord_leq to ord_compl,
     seq_perm_eq_ex -> ord_compl.perm_EX (modified = fixed),
     seq_sort_perm_ex -> ord_compl.sort_perm_EX (modified = fixed).
WIP: injF_restr_bij_EX.

Don't qualify idents from seq/path.
Add and prove size_ord_enum.
WIP: perm_ord_enum_sort.

Finite_family:
Don't qualify idents from seq/path.
TODWIP: seq_sort_perm_ex (to be fixed).

Add def ord_leq.
Rename path_sort_permut -> seq_sort_perm_ex.
WIP: seq_perm_eq_ex, seq_sort_perm_ex, injF_restr_bij_EX.

Modify def incrF (Nat.lt -> ltn).
Adapt proof of incrF_inj.
WIP: path_sort_permut, injF_restr_bij_EX.

Add and prove inj_equiv.

nat_compl:
Remove double nat_eq_leq (use Nat.le_0_r instead).
Rename nat_eq_leq -> nat_eq_le.

ord_compl:
Rename inj_ord_* -> injF_*.
Add and prove injF_le, surjF_le, lenPF_n0_alt.

Finite_family, Monoid_compl, Finite_dim:
Propagate new API (from nat_compl, ord_compl).

Finite_family:
Add and prove filterP_f_ord_correct_alt.
WIP: filterP_ord_incrF.

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).

Proof of filterPF_unfunF.
WIP: filterP_f_ord_incr.

Add and prove extendPF_permutF.
WIP: filterPF_unfunF (almost there?)

Some cleaning.
add and prove incl_RgF.

Finite_family:
filterPF_unfunF is necessary!
Add def filterP_f_ord.
Add and prove filt erP_f_ord_correct, filterP_f_ord_comp,
Modify filterPF_permutF, filterPF_funF, filterPF_unfunF.
Propagate modifications.
Proof of filterPF_permutF.
WIP: extendPF_refl, filterP_f_ord_comp_l, filterPF_unfunF.

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

Rm useless hypothesis.

Finite_family:
Some cleaning.
TODO: check filterPF_unfunF is really useful.

Add and prove comp_assoc.

Finite_family:
WIP: filterPF_unfunF (modified).
Propagate to filter_neqF_gen_unfunF{,_l}, filter_neqF_unfunF.

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

Modify def filterP_f_ord_n.

Finite_family:
Add and prove funF_comp.
Proof of filterPF_funF.

Rename filterP_f_ord -> filterP_f_ord_p.
Add def filterP_f_ord_n.
Add and prove filterP_f_ord_n_p.

Finite_family:
Propagate new API (from ord_compl).
WIP: filterPF_funF (statement hopefully fixed!).
TODO: fix filter_neqF_gen_funF{,_r}, filter_neqF_funF.

Add and prove f_inv_inj, f_inv_surj.

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

Finite_family:
Add defs eqF, neqF (fold them everywhere).
Rename funF_neq -> funF_neqF (modified),
       unfunF_neq -> unfunF_neqF,
       extendPF_funF_neq -> extendPF_funF_neqF,
       extendPF_equiv -> extendPF_unfunF_equiv,
       extendPF_unfunF_neq -> extendPF_unfunF_neqF.
Add and prove funF_equiv,
              extendPF_funF_{rev,equiv},
              extendPF_funF_neqF_{rev,equiv}.
WIP: filterPF_funF.

Rename f_inv_invol -> f_inv_id.
Add and prove f_inv_invol{,_alt}.

Finite_family:
Propagate new API (from Function_compl).
WIP: filterPF_unfunF.

Add and prove Rg_equiv, Rg_compl_equiv.

Finite_family:
Move stuff around.
Add and prove filter_neqF_gen_funF_r, filter_neqF_funF.

Add and prove Rg_compl.

Finite_family:
Generalize castF_eq_sym to any type.
Modify def extendPF.
Rename extendPF_unfunF -> extendPF_unfunF_neq.
Add and prove funF_neq, unfunF_neq,
              extendPF_funF, extendPF_funF_neq,
              extendPF_unfunF{,_rev}, extendPF_equiv,
              len_neqF_funF, filter_neqF_gen_funF.
WIP: filterPF_funF (was filterPF_ext_r_glop),
     filterPF_unfunF (was filterPF_extendPF).

Add and prove inj_comp_l, f_inv_invol.

ord_compl:
Final? version of def filterP_f_ord.
Modify filterP_f_ord_correct_{in,out}, filterP_f_ord_id.

Finite_family:
Modify filterPF_permutF (WIP),
       filterPF_{revF,moveF,transpF}.
WIP: filterPF_ext_r_glop (to be fixed),
     filterPF_extendPF.

Collect three defs of filterP_f_ord, all presumably unsatisfactory!

Modify def filterP_f_ord.
Adapt proofs of filterP_f_ord_correct_{in,out}, filterP_f_ord_id.

Finite_family:
Simplify proof of lenPF_permutF.
WIP: another def for filterP_f_ord.
Add and prove lenPF_permutF_f_inv_{l,r}.
WIP: filterPF_permutF.
Temporarily comment out filterPF_revF, {lenPF,filterPF}_{moveF,transpF}.