Add and prove f_zero_minus_opp_compat, f_opp_minus_plus_compat,
              f_plus_opp_minus_compat.

Sub_struct:
Proofs of sub{,_ms}_fun_rev.
Modify sub{,_ms}_{inj,surj,bij}_equiv.
Add and prove fct_sub_{inj,surj,bij}_{rev,equiv}.
              sub_{m,g,r,as}_fun_rev,
              {,fct_}sub_{m,g,r,as}_{inj,surj,bij}_{rev,equiv},
              {,fct_}sub_g_f_{opp,minus}_compat,
              fct_sub_ms_{inj,surj,bij}_{rev,equiv}.

Add alias classic_dec for excluded_middle_informative.

Finite_family, Finite_table, Monoid_compl, Ring_compl, AffineSpace,
  Sub_struct, Finite_dim, multi_index, FE:
Propagate new API (from logic_compl).

Make some arguments explicit.
Add and prove sub_{inj,surj,bij}_{rev,equiv},
              sub_ms_{inj,surj,bij}_{rev,equiv}.
WIP: sub_fun_rev, sub_ms_fun_rev.

P_approx_k:
Remove useless (use replace2F_equiv_def instead of replaceF_switch).

Add some doc.

Rename f_inv_correct_{l,r} -> f_inv_can_{l,r}.

Function_sub:
Add def involS.
Add and prove involS_injS, involS_bijS.
Rename f_invS_canS_l <-> f_invS_canS_r.
Add and prove f_invS_uniq_{l,r}, f_invS_{bijS,injS,surjS},
              f_invS_eq_equiv, f_invS_neq_equiv,
              f_invS_ext, f_invS_invol{,_alt},
              f_invS_id{,_rev,_equiv}.

ord_compl, Finite_family, ModuleSpace_compl, AffineSpace, Finite_dim,
  poly_Lagrange, P_approx_k, FE_LagP:
Propagate new API (from Function_compl).

FE_LagP:
Propagate new API (from Function_sub).

Shorten some proofs.
Add and prove f_inv_id_{l,r}.

Generalize funS_id.
Add and prove canS_id_{l,r}, bijS_id.

MonoidComp:
Propagate new APi (from Function_sub).

Add and prove bij_ex_uniq{,_rev}.
Simplify proof of bij_ex_uniq_equiv.

AffineSpace:
Simplify proofs using bij_ex_uniq_equiv.

Add and prove can_ext{_l,_r,},
              bij_ext, bij_comp_compat, bij_can_uniq_{l,r}.

AffineSpace:
Propagate new APi (from Function_compl).

Move stuff around.
Add and prove Rg_ext, surj_ext, surj_comp_{compat,reg}.

Function_sub:
Add and prove surjS_id, surjS_has_right_inv.

Add and prove inj_ext, inj_comp_{compat,reg}, inj_can_uniq_l.

ord_compl:
Propagate new API (from Function_compl).

Rename cancel_id -> can_equiv.
Add and prove comp_id, can_id.

Add and prove imp_not_{l,r}_{and,or}_equiv,
              not_imp_not_{l,r}_{and,or}_equiv.

Function_compl:
Add and prove surj_can_uniq_r, inj_contra_{rev,equiv}.

Function_sub:
Add and prove imS_dec,
              injS_id, injS_contra{,_rev,_equiv}, injS_equiv,
              injS_canS_uniq_l, comp_injS_r, surjS_canS_uniq_r,
              injS_has_left_inv.

Remove useless lemmas.

Function_sub:
Make some arguments implicit, others explicit.
Add def same_funS.
Add and prove same_funS_{refl,sym,trans},
              RgS{,_gen}_ext, funS_ext, injS_ext,
              surjS_ext, surjS_RgS_equiv,
              canS_ext{_l,_r,}, canS_{injS,surjS}, injS_canS_sym,
              bijS_ext, bijS_RgS, bijS_canS_uniq_{l,r},
              bijS_canS_sym, bijS_canS_bijS.
Rename surjS_equiv -> surjS_RgS_gen_equiv,
       surjS_equiv_alt -> surjS_RgS_equiv_alt.

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

sym_eq, Logic.eq_sym -> eq_sym.

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