nat_compl:

Some cleaning.
Move stuff around.
Add and prove nat_le_total, nat_lt_total_strict, le_neq_lt, nat_ltS.

ord_compl:
Simplify/compact some proofs.
Move stuff around.
Move is_orderedF stuff from Monoid_compl.
Rename is_orderedF* -> sortedF*,
       is_orderedF_S_aux -> sortedF_S_sortedF_aux,
       is_orderedF_S -> sortedF_S_sortedF.
Add def sortedF_S.
Modify sortedF_inj, sortedF_S_sortedF_aux, sortedF_S_sortedF.
Add and prove sortedF_sortedF_S, sortedF_equiv.
Add defs ord_le, ord_lt, ord_ltn.
Add and prove ord_le_{refl,antisym,trans,total},
              ord_lt_{irrefl,asym,trans,total_strict}.
Modify defs incrF{,_S}.
Proof of incrF_equiv.
Simplify proof of incrF_inj.

Finite_family:
Add defs PAF, PEF, notF, andF, orF, impF, equivF.
Add and prove PF_dec{,_l,_r}.
Simplify proofs of brF_dec{,_l,_r}.
Rename equivF -> equivFA.
Move is_orderedF_castF from Monoid_compl.
Rename is_orderedF_castF -> sortedF_castF,
       skipF_coupleF_{0,1} -> skipF_2{l,r},
       skipF_tripleF_{0,1,2} -> skipF_3{l,m,r}.
Add and prove PAF_ind_{l,r,skipF,skip2F,replaceF,replace2F},
              sortedF_castF_rev, sortedF_castF_equiv.
Rename incrF_Rg_eq_eq_aux -> incrF_Rg_le_0,
       incrF_Rg_eq_eq -> ext_fun_incrF_Rg.
Simplify proofs of Rg_0_liftF_S, incrF_Rg_le_0, ext_fun_incrF_Rg.

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

Monoid_compl:
Move is_orderedF stuff to ord_compl and Finite_family.
Simplify proof of concatnF_order.

multi_index:
Move stuff around.
Rename MO{2,n}_aux{1,2} -> MO{2,n}_correct{1,2}.
Fix MO2_correct{1,2}, MOn_correct2 (commented).
Rename MOn_neq -> MOn_irrefl (modified),
       MOn_total_order -> MOn_total_strict (modified).