Add prop_ext/proof_irrel, aliases for propositional_extensionality/proof_irrelevance.

Function_compl:
Rename bij_ex_uniq -> bij_ex_uniq_equiv.

Function_sub:
Add doc.
Move stuff around.
Modify def bijS.
Rename bijS_alt -> bijS_spec,
       bijS_ex -> bijS_ex_uniq_equiv (modified).
Rm double funS_comp.
Add and prove inj_S_equiv.

ord_compl, Finite_family, MonoidComp, AffineSpace, Sub_struct, Finite_dim,
  multi_index, poly_Lagrange, FE, FE_simplex, FE_LagP:
Propagate new API (from logic_compl, Function_compl, Function_sub).

ord_compl:
Make some arguments implicit.

{Monoid,Group,Ring,ModuleSpace}_compl, AffineSpace:
Add and prove inhabited_fct_{m,g,r,ms,as}.

Choose form for surjectivity and use the same with range (f x1 = x2).
Some internal renaming.

Function_sub:
Actually, bijS_ex needs "non-unique" choice.
Unify form of surjectivity (f x1 = x2).
Some internal renaming.
Split bijS_comp_reg in to bijS_comp_{injS,surjS}.

Finite_family, Monoid_compl, Sub_struct:
Propagate new API (from Function_compl).
Some internal renaming.

Tune required library files.
Add some documentation.
Move stuff around, factor arguments and compact/simplify some proofs.
Some style unification.

logic_compl:
Rename not_eq_sym_invol -> neq_sym_invol.
Add and prove iff_not_l_equiv,
              ex_EX (an alias for constructive_indefinite_description).

Subset_compl:
Use Lebesgue.Subset_dec and logic_compl instead of ClassicalEpsilon.

Function_compl:
Rename inj_comp_l -> comp_inj_l.
Add and prove fun_ext_contra{,_rev,_equiv}, surj_id, f_inv_id_{rev,equiv}.

Function_sub: WIP.

Sub_struct:
Propagate new API (from Subset_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.

Comment unused admitted results (and rename dmit -> glop).

Subset_system:
Add and prove Gen_Prod_Gen_Product.

Add and prove {widen,narrow,lift,lower}_S_inj,
              filterP_ord_ind_l_in_0_equiv, filterP_ord_ind_r_in_max_equiv.
WIP: filterP_ord_ind_l_in_n0.

Finite_family:
Nope!

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.

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

Compact some proofs.
Add todo about naming.

ord_compl:
More stable version of insert_concat_r_ord_0.

Finite_family:
Propagate new API (from ord_compl).

Add and prove RgS_comp.

Rename injS_inj -> inj_S_equiv,
       surjS_surj -> surj_S_equiv,
       bijS_bij -> bij_S_equiv.

Sub_struct, Finite_dim:
Propagate new API (from Function_sub).

Move stuff around.

Finite_family:
Rename ext_fun_incrF_Rg -> fun_ext_incrF_Rg.

Proof of filterP_ord_incrF_S.
WIP: sorted_ordP.

WIP: filterP_ord_incrF_S.

Add and prove map_nth_invF.
Proof of perm_EX.

WIP: perm_EX.

Add and prove ltn_asym.

ord_compl:
Add and prove ord_leq_{refl,antisym,trans},
              ord_ltn_{irrefl,asym,trans,total_strict}.

Finite_family:
Propagate new API (from ord_compl).

Add and prove skipF_2{l,r}0, skipF_3{l,m,r}{0,1},
              skipF_coupleF_{l,r}, skipF_tripleF_{l,m,r}.

multi_index:
Propagate new API (from Finite_family).

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

Some cleaning (dead code) + some todo.

Simplify proof.

ord_compl:
Add def incrF_S.
WIP: incrF_equiv.

Finite_family:
Proof of injF_restr_bij_EX.